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

[Vanessa McHale]

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 <mailto: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 <mailto: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
>         <mailto: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 <mailto:Libraries at haskell.org>
>         > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>         _______________________________________________
>         Libraries mailing list
>         Libraries at haskell.org <mailto:Libraries at haskell.org>
>         http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
>     _______________________________________________
>     Libraries mailing list
>     Libraries at haskell.org <mailto: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/20191224/772ce015/attachment.html>