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@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@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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries