<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>You can use hlint to ban a function (such as undefined) in a
particular codebase. I use it to avoid releasing packages without
a real error message.</p>
<p>Cheers,<br>
Vanessa<br>
</p>
<div class="moz-cite-prefix">On 12/23/19 8:51 PM, Tikhon Jelvis
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAJN5CVKAwpGG9iTZAF1S278yT3t_SuP-NoG4Gt29JmxfjrrxvA@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="auto">In our codebase at work, undefined had a warning
and we have a value called unreachable for cases where it makes
sense semantically. We use undefined during development and the
warning acts as both a safety net and a list of todos to fix
before the code is ready to merge.</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Mon, Dec 23, 2019, 12:26
Carter Schonwald <<a
href="mailto:carter.schonwald@gmail.com"
moz-do-not-send="true">carter.schonwald@gmail.com</a>>
wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr">
<div>i agree with richard here: <br>
</div>
<div><br>
</div>
<div>i'd even say it more strongly: <br>
</div>
<div>totality is a global property, any "local only "
mechanism will backfire on some valid total code.</div>
<div><br>
</div>
<div>worst of all: any theorem prover extracted code will be
rejected :) <br>
</div>
<div>(well, at least the sort coq/agda extract to,
isabelle/hol code tends to have less unsafe coerce party
time, though still would likely fail any "local" totally
rules of thumb).<br>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Mon, Dec 23, 2019 at
10:48 AM Richard Eisenberg <<a
href="mailto:rae@richarde.dev" target="_blank"
rel="noreferrer" moz-do-not-send="true">rae@richarde.dev</a>>
wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid
rgb(204,204,204);padding-left:1ex">I have not seen a
serious proposal for TotalHaskell before. It would be a
great thing to have, but my guess is that at least two PhD
students would have to be sacrificed to the cause. There
are *many* ways that Haskell is a non-total language.<br>
<br>
Here are a few:<br>
<br>
- general recursion (including definitions like loop =
loop)<br>
- well-founded recursion (where the recursive calls are
on structurally smaller arguments) is ok, though<br>
- but not on infinite data<br>
- well-guarded corecursion (like `ones = 1 : ones`) is
also ok<br>
- recursive type-class dictionaries allows (I think)
unbounded recursion<br>
- exceptions<br>
- incomplete pattern matches<br>
- unless GADT restrictions say that the match is
actually total<br>
- incomplete uni-pattern matches<br>
- unless GADT restrictions say that the match is
actually total<br>
- partial record selectors<br>
- non-strictly-positive datatypes<br>
- Typeable allows you to simulate non-strictly-positive
datatypes (see Sec. 7 of <a
href="https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1002&context=compsci_pubs"
rel="noreferrer noreferrer" target="_blank"
moz-do-not-send="true">https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1002&context=compsci_pubs</a>)<br>
- Girard's paradox (because we have Type :: Type), though
it is not known whether this is encodable in Haskell. See
<a
href="https://link.springer.com/chapter/10.1007/BFb0014058"
rel="noreferrer noreferrer" target="_blank"
moz-do-not-send="true">https://link.springer.com/chapter/10.1007/BFb0014058</a><br>
- -fdefer-type-errors<br>
<br>
Some of these are easy enough to stamp out, but others may
be harder. And I'm sure I'm missing some cases. I am *not*
trying to say we shouldn't do anything in this direction
-- far from it. However, one should proceed in this
direction with eyes open.<br>
<br>
Richard<br>
<br>
> On Dec 23, 2019, at 8:12 AM, Vilem Liepelt <<a
href="mailto:vliepelt@futurefinance.com" target="_blank"
rel="noreferrer" moz-do-not-send="true">vliepelt@futurefinance.com</a>>
wrote:<br>
> <br>
> <br>
>> I assume a TotalHaskell pragma was proposed in
the past. Would this help?<br>
> <br>
> Yes, in fact I think this is even better. Does
"total" refer to exhaustive pattern matching and absence
of (possible) exceptions?<br>
> <br>
> We might want to have such a pragma on a
function-by-function basis as well as whole-module.<br>
> <br>
> My company has committed to letting me work on GHC a
couple of days each month, so I'd be up to work on this,
although I'd need someone to hold my hand as I haven't
done this before.<br>
> _______________________________________________<br>
> Libraries mailing list<br>
> <a href="mailto:Libraries@haskell.org"
target="_blank" rel="noreferrer" moz-do-not-send="true">Libraries@haskell.org</a><br>
> <a
href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries"
rel="noreferrer noreferrer" target="_blank"
moz-do-not-send="true">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
<br>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank"
rel="noreferrer" moz-do-not-send="true">Libraries@haskell.org</a><br>
<a
href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries"
rel="noreferrer noreferrer" target="_blank"
moz-do-not-send="true">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote>
</div>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank"
rel="noreferrer" moz-do-not-send="true">Libraries@haskell.org</a><br>
<a
href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries"
rel="noreferrer noreferrer" target="_blank"
moz-do-not-send="true">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Libraries mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Libraries@haskell.org">Libraries@haskell.org</a>
<a class="moz-txt-link-freetext" href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a>
</pre>
</blockquote>
</body>
</html>