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

[Edward Kmett]

I'm much more in favor of pushing folks that want warnings of this sort of
behavior towards custom HLint rules for banning behavior (which can be done
today, but probably comes across as too weak) or towards seeking a general
mechanism to name a set of methods you'd like to explicitly warn about
during compilation time (so that mechanism could be more uniformly applied
across third-party code bases, but which requires a design and GHC
engineering effort) over applying a WARNING pragma as a blunt instrument to
this particular problem.

(As an aside, let x = x in x can throw a NonTermination exception without
ever invoking any explicit throwing mechanism, depending on how nice your
runtime system wants to be, so being "exception-free" here is confusing
phrasing to me.)

WARNING as it stands is far too strong. There are plenty of cases where
they are the only thing you can do, due to limitations of the totality
checker or invariants that Haskell can't express holding behind your back.

A rule of thumbs I've tried to keep in mind towards existing warnings and
deprecation efforts is that a WARNING or DEPRECATED pragma that leaves you
with no alternative but to listen to the compiler scream even when you are
doing your utmost to avoid it short of disabling all warnings is a badly
designed warning or deprecation.

-Edward




On Mon, Dec 23, 2019 at 11:04 AM Vilem Liepelt <vliepelt at futurefinance.com>
wrote:

> I agree with your assessment, Richard, but my (possibly flawed)
> understanding is that in the Haskell community "totality" does not have the
> same meaning as in mathematics/PLT—Haskellers use "total" for the property
> "doesn't throw non-exhaustive pattern match errors" or perhaps "doesn't
> throw any exceptions at all" vs "terminating" for the property "doesn't
> loop infinitely". [citation needed]
>
> Hence I understood Henning's proposal to refer to the notion of
> "exception-free". This would already be a very useful property and I
> suspect would be easier to solve. Yes, complete pattern matches are
> undecidable in the presence of GADTs, but can't we simply build on GHC's
> existing heuristics?
>
> Would this really be a pragma or would it be a language */restriction/*
>  (heh)?
>
> Regarding nontermination, I would be grateful if Haskell at least had an
> option for explicit let-rec...
>
> On 23 Dec 2019, at 17:44, Richard Eisenberg <rae at richarde.dev> wrote:
>
>  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
>
>
> _______________________________________________
> 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/20191225/a919fe34/attachment.html>