WARNING pragmas in `Prelude.undefined` and `Prelude.error`
Locked
12
12
WARNING pragmas in `Prelude.undefined` and `Prelude.error`
 
|
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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
|
|
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 <[hidden email]> wrote: Has there been any discussion about adding WARNING pragmas to `Prelude.undefined` and `Prelude.error`, as done in some custom preludes? _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
|
|
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 . <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
In reply to this post by Vilem Liepelt
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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
In reply to this post by Zemyla
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 . <[hidden email] > <mailto:[hidden email]>> 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 > <[hidden email] <mailto:[hidden email]>> 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 > [hidden email] <mailto:[hidden email]> > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries > > _______________________________________________ > Libraries mailing list > [hidden email] <mailto:[hidden email]> > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries > > > _______________________________________________ > Libraries mailing list > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries > Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
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.
> On 23 Dec 2019, at 13:36, Andreas Abel <[hidden email]> wrote: > > 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 . <[hidden email] <mailto:[hidden email]>> 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 >> <[hidden email] <mailto:[hidden email]>> 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 >> [hidden email] <mailto:[hidden email]> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries >> _______________________________________________ >> Libraries mailing list >> [hidden email] <mailto:[hidden email]> >> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries >> _______________________________________________ >> Libraries mailing list >> [hidden email] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries > _______________________________________________ > Libraries mailing list > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
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? _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
> 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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
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 <[hidden email]> 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 > [hidden email] > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
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...
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
In reply to this post by chessai .
Some warnings are not included in -Wall (for instance -Wincomplete-uni-patterns). New warning flags can be added without breaking any code. Best regards, Daniel Am So., 22. Dez. 2019 um 12:50 Uhr schrieb chessai . <[hidden email]>:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
In reply to this post by Zemyla
> On 22 Dec 2019, at 14:15, Zemyla <[hidden email]> 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 [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
In reply to this post by Daniel Díaz Casanueva
> On 23 Dec 2019, at 18:10, Daniel Díaz Casanueva <[hidden email]> 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? _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
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`. Am Mo., 23. Dez. 2019 um 17:33 Uhr schrieb Vilem Liepelt <[hidden email]>:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
In reply to this post by Richard Eisenberg-5
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 <[hidden email]> 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. _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
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 <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
In reply to this post by Daniel Díaz Casanueva
> On 23 Dec 2019, at 21:48, Daniel Díaz Casanueva <[hidden email]> 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. :) _______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
In reply to this post by Tikhon Jelvis
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, On 12/23/19 8:51 PM, Tikhon Jelvis
wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
excellent point! On Tue, Dec 24, 2019 at 11:53 AM Vanessa McHale <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`
|
|
In reply to this post by Vilem Liepelt
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 <[hidden email]> wrote:
_______________________________________________ Libraries mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries |
«
Return to Haskell - Libraries
|
1 view|%1 views
| Free forum by Nabble | Edit this page |