<div dir="ltr"><div>excellent point! <br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Dec 24, 2019 at 11:53 AM Vanessa McHale <<a href="mailto:vamchale@gmail.com">vamchale@gmail.com</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">
<div 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>On 12/23/19 8:51 PM, Tikhon Jelvis
wrote:<br>
</div>
<blockquote type="cite">
<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" target="_blank">carter.schonwald@gmail.com</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">
<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" rel="noreferrer" target="_blank">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">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">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" rel="noreferrer" target="_blank">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" rel="noreferrer" target="_blank">Libraries@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
<br>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" rel="noreferrer" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote>
</div>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" rel="noreferrer" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote>
</div>
<br>
<fieldset></fieldset>
<pre>_______________________________________________
Libraries mailing list
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a>
</pre>
</blockquote>
</div>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div>