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

[Vilem Liepelt]

I agree with your assessment, Richard, but my (possibly flawed) understanding is that in the Haskell community "totality" does not have the same meaning as in mathematics/PLT—Haskellers use "total" for the property "doesn't throw non-exhaustive pattern match errors" or perhaps "doesn't throw any exceptions at all" vs "terminating" for the property "doesn't loop infinitely". [citation needed]

Hence I understood Henning's proposal to refer to the notion of "exception-free". This would already be a very useful property and I suspect would be easier to solve. Yes, complete pattern matches are undecidable in the presence of GADTs, but can't we simply build on GHC's existing heuristics?

Would this really be a pragma or would it be a language /restriction/ (heh)?

Regarding nontermination, I would be grateful if Haskell at least had an option for explicit let-rec...

> On 23 Dec 2019, at 17:44, Richard Eisenberg <rae at richarde.dev> wrote:
> 
>  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 <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 <https://link.springer.com/chapter/10.1007/BFb0014058>
> - -fdefer-type-errors

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20191223/9799ea30/attachment.html>