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

[Richard Eisenberg]

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 at 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries