Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`

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 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 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