<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">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" 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" 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" 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" 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>
<br>
_______________________________________________<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>