On Mon, Dec 23, 2019, 12:26 Carter Schonwald <carter.schonwald@gmail.com> wrote:

i agree with richard here:

i'd even say it more strongly:

totality is a global property, any "local only " mechanism will backfire on some valid total code.

worst of all: any theorem prover extracted code will be rejected :)

(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).

On Mon, Dec 23, 2019 at 10:48 AM Richard Eisenberg <rae@richarde.dev> wrote:

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.

Here are a few:

- general recursion (including definitions like loop = loop)
- well-founded recursion (where the recursive calls are on structurally smaller arguments) is ok, though
- but not on infinite data
- well-guarded corecursion (like `ones = 1 : ones`) is also ok
- recursive type-class dictionaries allows (I think) unbounded recursion
- exceptions
- incomplete pattern matches
- unless GADT restrictions say that the match is actually total
- incomplete uni-pattern matches
- unless GADT restrictions say that the match is actually total
- partial record selectors
- non-strictly-positive datatypes
- Typeable allows you to simulate non-strictly-positive datatypes (see Sec. 7 of https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1002&context=compsci_pubs)
- Girard's paradox (because we have Type :: Type), though it is not known whether this is encodable in Haskell. See https://link.springer.com/chapter/10.1007/BFb0014058
- -fdefer-type-errors

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.

Richard

> On Dec 23, 2019, at 8:12 AM, Vilem Liepelt <vliepelt@futurefinance.com> wrote:
>
>
>> I assume a TotalHaskell pragma was proposed in the past. Would this help?
>
> Yes, in fact I think this is even better. Does "total" refer to exhaustive pattern matching and absence of (possible) exceptions?
>
> We might want to have such a pragma on a function-by-function basis as well as whole-module.
>
> 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.
> _______________________________________________
> Libraries mailing list
> Libraries@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________
Libraries mailing list
Libraries@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries