I am missing some context of this discussion, but if this is the question of whether using `undefined` and `error` can be legitimate, yes they can. If you know your invariants, you might want to write fromMaybe undefined $ lookup key map or Map.findWithDefault undefined key map knowing you put the key into the map and the lookup cannot fail. On 2019-12-22 13:15, Zemyla wrote:

The most common legitimate usage for undefined I have is strictness:

func x y | x `seq` False = undefined func x y = ...

There's nothing else that would go there, and when it's compiled, the reference to undefined disappears.

On Sun, Dec 22, 2019, 05:50 chessai . mailto:chessai1996@gmail.com> wrote:

Right, it's been discussed before IIRC, and i know I've certainly given it passing thoughts. I think this isn't worth it because of breakage. Many people use -Wall -Werror, so I see this as a no-go.

Thanka

On Sun, Dec 22, 2019, 6:45 AM Vilem Liepelt mailto:vliepelt@futurefinance.com> wrote:

Has there been any discussion about adding WARNING pragmas to `Prelude.undefined` and `Prelude.error`, as done in some custom preludes?

I suppose this hasn't been done yet to avoid breaking existing code which makes "legitimate" use of those helpers? _______________________________________________ Libraries mailing list Libraries@haskell.org mailto:Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org mailto:Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

On Mon, 23 Dec 2019, Vilem Liepelt wrote:

I agree that `error`/`undefined` can be legitimate; however often this legitimacy rests on invariants that aren't necessary stable under change-types-and-fix-errors-until-things-type-check style refactoring! So after refactoring I'd like to switch on my `error`/`undefined` warnings temporarily.

I assume a TotalHaskell pragma was proposed in the past. Would this help?

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

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 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 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

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

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

excellent point! On Tue, Dec 24, 2019 at 11:53 AM Vanessa McHale 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 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 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 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________ Libraries mailing listLibraries@haskell.orghttp://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

The idiom of using undefined to replace BangPatterns has a few benefits, which is why it gets used in libraries like bytestring. It doesn't require a language extension and applies a bit nicer in macro expansion because it infects one line of your patterns rather than either mangling all pattern matches or relying on subtleties about whether or not the pattern match earlier was enough to 'forget' the strictness of a later pattern when it isn't strict in a subsequent pattern. foo !(Bar x) !(Bar y) = ... foo y w = ... am I strict in w? foo x y | seq x (seq y False) = undefined foo (Bar x) (Bar y) = ... foo y w = ... is definitely strict in w Other usecases are for working with combinators like sizeOf, alignment, bitSize, bitSizeMaybe, finiteBitSize, or doing things like initializing self-referential IORef structures whenever you do have to tie the knot strictly, etc. In the former cases you can argue that the API should change to take a Proxy, then spend a couple of years driving that change process through, as most of them affect the current language report, but in the latter case you're basically stuck with either embracing momentary partiality and knowledge of lack of escape or working with inaccurately weak types after the structure is initialized, forever. -Edward On Mon, Dec 23, 2019 at 11:30 AM Vilem Liepelt wrote:

...

On 22 Dec 2019, at 14:15, Zemyla wrote:

The most common legitimate usage for undefined I have is strictness:

func x y | x `seq` False = undefined func x y = ...

There's nothing else that would go there, and when it's compiled, the reference to undefined disappears.

Is this (better than | different from) using BangPatterns? _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

On 23 Dec 2019, at 18:10, Daniel Díaz Casanueva wrote:

Some warnings are not included in -Wall (for instance -Wincomplete-uni-patterns). New warning flags can be added without breaking any code.

Agreed, Daniel, but if we added a warning/deprecation pragma to the library (which is what I had asked about), then this would get triggered by -Wdeprecations which is part of -Wall. I'm not sure adding a flag specifically for usages of `error`/`undefined` makes much sense. E.g. what if I bind those names to genuine values?

On 23 Dec 2019, at 21:48, Daniel Díaz Casanueva wrote:

Oh, I see. Sorry. I totally misunderstood the proposal. I should have read more carefully.

I think undefined and error are useful functions to have, so why adding WARNING to them? For example, you can fold an infinite structure `xs` with `foldr f undefined xs` (for some proper `f`) without needing to define or look for an alternative to `Data.Foldable.foldr`.

Yes, as long as the structure really is infinite. However the types don't guarantee or even suggest this, so this can easily blow up after a refactor that doesn't take this unwritten rule into consideration. If `undefined` came with a WARNING, then that might encourage you to try to express your solution with a proper coinductive data structure. :)

To add, I know quite a few developers who, during development, use undefined in place of an "I don't know yet" to get the program compiling, then perhaps might add an underscore _undefined to determine the type. Using undefined is perhaps less preferable to using :reload! but it's quite a bit to type and :r! doesn't work. On 22/12/19 10:26 pm, Francesco Ariis wrote:

On Sun, Dec 22, 2019 at 01:44:58PM +0200, Vilem Liepelt wrote:

...

Has there been any discussion about adding WARNING pragmas to `Prelude.undefined` and `Prelude.error`, as done in some custom preludes?

I suppose this hasn't been done yet to avoid breaking existing code which makes "legitimate" use of those helpers? `undefined` is useful when you want to check types in, e.g. ghcid, without writing a function in full. With -Wall on, that Warning could become annoying fast.

---

Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries