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

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
22 messages Options
12
Reply | Threaded
Open this post in threaded view
|

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

Vilem Liepelt
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
Reply | Threaded
Open this post in threaded view
|

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

chessai .
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?

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

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Zemyla
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:
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?

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
_______________________________________________
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
Reply | Threaded
Open this post in threaded view
|

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

Francesco Ariis
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
Reply | Threaded
Open this post in threaded view
|

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

Andreas Abel
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
Reply | Threaded
Open this post in threaded view
|

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

Vilem Liepelt
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
Reply | Threaded
Open this post in threaded view
|

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

Henning Thielemann

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
Reply | Threaded
Open this post in threaded view
|

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

Vilem Liepelt

> 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
Reply | Threaded
Open this post in threaded view
|

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

Richard Eisenberg-5
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
Reply | Threaded
Open this post in threaded view
|

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

Vilem Liepelt
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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Daniel Díaz Casanueva
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]>:
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?

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
_______________________________________________
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
Reply | Threaded
Open this post in threaded view
|

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

Vilem Liepelt
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
Reply | Threaded
Open this post in threaded view
|

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

Vilem Liepelt
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
Reply | Threaded
Open this post in threaded view
|

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

Daniel Díaz Casanueva
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]>:

> 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
Reply | Threaded
Open this post in threaded view
|

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

Carter Schonwald
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.

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

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Tikhon Jelvis
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:
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.

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
_______________________________________________
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
Reply | Threaded
Open this post in threaded view
|

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

Vilem Liepelt
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
Reply | Threaded
Open this post in threaded view
|

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

Vanessa McHale-2
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,
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 <[hidden email]> 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 <[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.

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
_______________________________________________
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
Reply | Threaded
Open this post in threaded view
|

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

Carter Schonwald
excellent point!


On Tue, Dec 24, 2019 at 11:53 AM Vanessa McHale <[hidden email]> 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 <[hidden email]> 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 <[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.

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

_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
Reply | Threaded
Open this post in threaded view
|

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

Edward Kmett-2
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:
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 <[hidden email]> 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
[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
12