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

[Carter Schonwald]

excellent point!


On Tue, Dec 24, 2019 at 11:53 AM Vanessa McHale <vamchale at gmail.com> wrote:

> You can use hlint to ban a function (such as undefined) in a particular
> codebase. I use it to avoid releasing packages without a real error message.
>
> Cheers,
> Vanessa
> On 12/23/19 8:51 PM, Tikhon Jelvis wrote:
>
> 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
>>
>
> _______________________________________________
> Libraries mailing listLibraries at haskell.orghttp://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/20191224/a65d03f7/attachment.html>