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

[Carter Schonwald]

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 at 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 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
>
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20191223/c955a59c/attachment.html>