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

[Tikhon Jelvis]

In our codebase at work, undefined had a warning and we have a value called
unreachable for cases where it makes sense semantically. We use undefined
during development and the warning acts as both a safety net and a list of
todos to fix before the code is ready to merge.

On Mon, Dec 23, 2019, 12:26 Carter Schonwald <carter.schonwald at 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 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
>>
> _______________________________________________
> 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/93d0d152/attachment.html>