Allowing (Char ~ Bool => Void)?
Is there a good reason that GHC doesn't allow any value of type (Char
~ Bool => Void), even undefined?
There are various use cases for this. It's allowed indirectly, via
GADT pattern matches -- "foo :: Is Char Bool -> Void; foo x = case x
of {}" (with EmptyCase in HEAD) -- but not directly.
One thing this prevents, for instance, is CPSifying GADTs:
data Foo a = a ~ Char => A | a ~ Bool => B -- valid
newtype Bar a = Bar { runBar :: forall r. (a ~ Char => r) -> (a ~
Bool => r) -> r } -- unusable
Trying to use a type like the latter in practice runs into problems
quickly because one needs to provide an absurd value of type (Char ~
Bool => r), which is generally impossible (even if we're willing to
cheat with ⊥!). It seems that this sort of thing should be doable.
Shachaf
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Allowing (Char ~ Bool => Void)?
Though I've never run into the problem Shachaf mentions, this certainly seems
useful. However, when testing Shachaf's code, I get the same error that I get
when writing an impossible branch of a case statement. I imagine that the same
code in GHC powers both scenarios, so any change would have to be careful to
preserve the case-branch behavior, which (I think) is useful.
Perhaps a general solution to this problem is to have some new term construct
"contra" (supply a better name please!) that can be used only when there is an
inconsistent equality in the context but can typecheck at any type. With
"contra", we could allow impossible case branches, because now there would be
something sensible to put there. This would be an alternate effective solution
to long-standing bug #3927, which is about checking exhaustiveness of case
matches.
Richard
On Mar 24, 2013, at 5:16 AM, Shachaf Ben-Kiki wrote:
> Is there a good reason that GHC doesn't allow any value of type (Char
> ~ Bool => Void), even undefined?
>
> There are various use cases for this. It's allowed indirectly, via
> GADT pattern matches -- "foo :: Is Char Bool -> Void; foo x = case x
> of {}" (with EmptyCase in HEAD) -- but not directly.
>
> One thing this prevents, for instance, is CPSifying GADTs:
>
>data Foo a = a ~ Char => A | a ~ Bool => B -- valid
>newtype Bar a = Bar { runBar :: forall r. (a ~ Char => r) -> (a ~
> Bool => r) -> r } -- unusable
>
> Trying to use a type like the latter in practice runs into problems
> quickly because one needs to provide an absurd value of type (Char ~
> Bool => r), which is generally impossible (even if we're willing to
> cheat with ⊥!). It seems that this sort of thing should be doable.
>
>Shachaf
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Allowing (Char ~ Bool => Void)?
On Sun, Mar 24, 2013 at 10:49:24AM -0400, Richard Eisenberg wrote:
> Though I've never run into the problem Shachaf mentions, this certainly seems
> useful. However, when testing Shachaf's code, I get the same error that I get
> when writing an impossible branch of a case statement. I imagine that the
> same code in GHC powers both scenarios, so any change would have to be
> careful to preserve the case-branch behavior, which (I think) is useful.
>
> Perhaps a general solution to this problem is to have some new term
> construct "contra" (supply a better name please!) that can be used
> only when there is an inconsistent equality in the context but can
> typecheck at any type. With "contra", we could allow impossible case
> branches, because now there would be something sensible to put
> there. This would be an alternate effective solution to
> long-standing bug #3927, which is about checking exhaustiveness of
> case matches.
+1 for contra. Alternative name suggestions: 'exfalso', 'shazam',
'pizza'.
-Brent
>
> On Mar 24, 2013, at 5:16 AM, Shachaf Ben-Kiki wrote:
>
> > Is there a good reason that GHC doesn't allow any value of type (Char
> > ~ Bool => Void), even undefined?
> >
> > There are various use cases for this. It's allowed indirectly, via
> > GADT pattern matches -- "foo :: Is Char Bool -> Void; foo x = case x
> > of {}" (with EmptyCase in HEAD) -- but not directly.
> >
> > One thing this prevents, for instance, is CPSifying GADTs:
> >
> >data Foo a = a ~ Char => A | a ~ Bool => B -- valid
> >newtype Bar a = Bar { runBar :: forall r. (a ~ Char => r) -> (a ~
> > Bool => r) -> r } -- unusable
> >
> > Trying to use a type like the latter in practice runs into problems
> > quickly because one needs to provide an absurd value of type (Char ~
> > Bool => r), which is generally impossible (even if we're willing to
> > cheat with ⊥!). It seems that this sort of thing should be doable.
> >
> >Shachaf
> >
> > ___
> > Glasgow-haskell-users mailing list
> > Glasgow-haskell-users@haskell.org
> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> >
>
>
> ___
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users@haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Allowing (Char ~ Bool => Void)?
What precisely is the proposal here? That "unreachable code" be a warning
rather than an error?
Would you care to make a ticket with a clear specification? Thanks!
Simon
| -Original Message-
| From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell-
| users-boun...@haskell.org] On Behalf Of Richard Eisenberg
| Sent: 24 March 2013 14:49
| To: Shachaf Ben-Kiki
| Cc: glasgow-haskell-users
| Subject: Re: Allowing (Char ~ Bool => Void)?
|
| Though I've never run into the problem Shachaf mentions, this certainly
| seems useful. However, when testing Shachaf's code, I get the same error
| that I get when writing an impossible branch of a case statement. I
| imagine that the same code in GHC powers both scenarios, so any change
| would have to be careful to preserve the case-branch behavior, which (I
| think) is useful.
|
| Perhaps a general solution to this problem is to have some new term
| construct "contra" (supply a better name please!) that can be used only
| when there is an inconsistent equality in the context but can typecheck
| at any type. With "contra", we could allow impossible case branches,
| because now there would be something sensible to put there. This would
| be an alternate effective solution to long-standing bug #3927, which is
| about checking exhaustiveness of case matches.
|
| Richard
|
| On Mar 24, 2013, at 5:16 AM, Shachaf Ben-Kiki wrote:
|
| > Is there a good reason that GHC doesn't allow any value of type (Char
| > ~ Bool => Void), even undefined?
| >
| > There are various use cases for this. It's allowed indirectly, via
| > GADT pattern matches -- "foo :: Is Char Bool -> Void; foo x = case x
| > of {}" (with EmptyCase in HEAD) -- but not directly.
| >
| > One thing this prevents, for instance, is CPSifying GADTs:
| >
| >data Foo a = a ~ Char => A | a ~ Bool => B -- valid
| >newtype Bar a = Bar { runBar :: forall r. (a ~ Char => r) -> (a ~
| > Bool => r) -> r } -- unusable
| >
| > Trying to use a type like the latter in practice runs into problems
| > quickly because one needs to provide an absurd value of type (Char ~
| > Bool => r), which is generally impossible (even if we're willing to
| > cheat with ⊥!). It seems that this sort of thing should be doable.
| >
| >Shachaf
| >
| > ___
| > Glasgow-haskell-users mailing list
| > Glasgow-haskell-users@haskell.org
| > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
| >
|
|
| ___
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Allowing (Char ~ Bool => Void)?
I would call this more of an idea than a proposal -- I'm not advocating that
it's necessarily the right thing, but one possible solution both to Shachaf's
original question and the problem of spurious warnings about bogus case
branches.
The idea is to introduce some new keyword, which I've called "contra", which
has the type (a ~ b) => c, where a cannot unify with b (and c is totally
unconstrained). Currently, whenever such an equality (a ~ b) is in the context,
GHC issues an error and prevents any further code. This is often good behavior
of a compiler, to prevent people from writing impossible code. However, Shachaf
found a case where it would be nice to have code that executes in an
inconsistent context. And, if we had contra, then we could just stick contra in
any inconsistent pattern matches, and there would be no need to fix the
warnings about incomplete pattern matches.
For example:
> data Nat = Zero | Succ Nat
> data SNat :: Nat -> * where
> SZero :: SNat Zero
> SSucc :: SNat n -> SNat (Succ n)
>
> safePred :: SNat (Succ n) -> SNat n
> safePred (SSucc n) = n
> safePred SZero = contra
(Seeing the code here, perhaps "impossible" is a better name.)
The last clause of safePred is indeed impossible. GHC issues an error on the
code above. If we remove the last line, GHC (rightly) does not issue a warning
about an incomplete pattern match. But, as documented on Trac #3927, there are
other places where GHC does issue a warning about missing impossible branches.
With contra, we could fill out such pattern matches and suppress the warning.
When I initially wrote up my "contra" idea, I was remembering a case where GHC
did not issue a warning on an inconsistent pattern match. In the process of
writing this email, I found that old case, and I realized that it was my fault,
not GHC's. I had originally thought that GHC's "impossible code" identification
feature was incomplete, but now perhaps I was wrong. If GHC can always detect
impossible code, the "contra" idea is less appealing than it once was to me,
though it would still solve Shachaf's problem.
Does this clarify the idea?
Richard
On Apr 3, 2013, at 1:49 PM, Simon Peyton-Jones wrote:
> What precisely is the proposal here? That "unreachable code" be a warning
> rather than an error?
>
> Would you care to make a ticket with a clear specification? Thanks!
>
> Simon
>
> | -Original Message-
> | From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell-
> | users-boun...@haskell.org] On Behalf Of Richard Eisenberg
> | Sent: 24 March 2013 14:49
> | To: Shachaf Ben-Kiki
> | Cc: glasgow-haskell-users
> | Subject: Re: Allowing (Char ~ Bool => Void)?
> |
> | Though I've never run into the problem Shachaf mentions, this certainly
> | seems useful. However, when testing Shachaf's code, I get the same error
> | that I get when writing an impossible branch of a case statement. I
> | imagine that the same code in GHC powers both scenarios, so any change
> | would have to be careful to preserve the case-branch behavior, which (I
> | think) is useful.
> |
> | Perhaps a general solution to this problem is to have some new term
> | construct "contra" (supply a better name please!) that can be used only
> | when there is an inconsistent equality in the context but can typecheck
> | at any type. With "contra", we could allow impossible case branches,
> | because now there would be something sensible to put there. This would
> | be an alternate effective solution to long-standing bug #3927, which is
> | about checking exhaustiveness of case matches.
> |
> | Richard
> |
> | On Mar 24, 2013, at 5:16 AM, Shachaf Ben-Kiki wrote:
> |
> | > Is there a good reason that GHC doesn't allow any value of type (Char
> | > ~ Bool => Void), even undefined?
> | >
> | > There are various use cases for this. It's allowed indirectly, via
> | > GADT pattern matches -- "foo :: Is Char Bool -> Void; foo x = case x
> | > of {}" (with EmptyCase in HEAD) -- but not directly.
> | >
> | > One thing this prevents, for instance, is CPSifying GADTs:
> | >
> | >data Foo a = a ~ Char => A | a ~ Bool => B -- valid
> | >newtype Bar a = Bar { runBar :: forall r. (a ~ Char => r) -> (a ~
> | > Bool => r) -> r } -- unusable
> | >
> | > Trying to use a type like the latter in practice runs into problems
> | > quickly because one needs to provide an absurd value of type (Char ~
> | > Bool => r), which is generally impossible (even if we're willing to
> | > cheat with ⊥!). It seems that this sort of thing should be doable.
RE: Allowing (Char ~ Bool => Void)?
| The idea is to introduce some new keyword, which I've called "contra",
| which has the type (a ~ b) => c, where a cannot unify with b (and c is
| totally unconstrained).
So you do not mean
contra :: forall abc. (a~b) => c
(where obviously a and b will unify). You mean rather
contra :: forall c. (Int ~ Bool) => c
or something like that.
| And, if we had
| contra, then we could just stick contra in any inconsistent pattern
| matches, and there would be no need to fix the warnings about incomplete
| pattern matches.
This part I don't understand *at all*! For example:
| > data Nat = Zero | Succ Nat
| > data SNat :: Nat -> * where
| > SZero :: SNat Zero
| > SSucc :: SNat n -> SNat (Succ n)
| >
| > safePred :: SNat (Succ n) -> SNat n
| > safePred (SSucc n) = n
| > safePred SZero = contra
From the last equation we get the constraint
(Zero ~ Succ n) => (Int ~ Bool)
(assuming my type for contra). The presence of an insoluble contraint after the
=> does not make it the slightest bit easier to suppress the error that current
arises from the insoluble given constraint before the =>.
I suppose you could have a magic constraint INSOLUBLE, say, with
contra :: INSOLUBLE => c
which had the effect of suppressing any enclosing "impossible branch" failure
error reports. It's not clear how far out it would go. What about
safePred SZero = if ... then contra else True
or
safePred SZero = case .. of { ...some other GADT matching... }
I can't say I'm enthusiastic here.
I WOULD like someone to help beef up the pattern-match overlap detector in the
desugarer. That would be really useful.
Simon
| -Original Message-
| From: Richard Eisenberg [mailto:e...@cis.upenn.edu]
| Sent: 03 April 2013 19:59
| To: Simon Peyton-Jones
| Cc: Shachaf Ben-Kiki; glasgow-haskell-users
| Subject: Re: Allowing (Char ~ Bool => Void)?
|
| I would call this more of an idea than a proposal -- I'm not advocating
| that it's necessarily the right thing, but one possible solution both to
| Shachaf's original question and the problem of spurious warnings about
| bogus case branches.
|
| The idea is to introduce some new keyword, which I've called "contra",
| which has the type (a ~ b) => c, where a cannot unify with b (and c is
| totally unconstrained). Currently, whenever such an equality (a ~ b) is
| in the context, GHC issues an error and prevents any further code. This
| is often good behavior of a compiler, to prevent people from writing
| impossible code. However, Shachaf found a case where it would be nice to
| have code that executes in an inconsistent context. And, if we had
| contra, then we could just stick contra in any inconsistent pattern
| matches, and there would be no need to fix the warnings about incomplete
| pattern matches.
|
| For example:
|
| > data Nat = Zero | Succ Nat
| > data SNat :: Nat -> * where
| > SZero :: SNat Zero
| > SSucc :: SNat n -> SNat (Succ n)
| >
| > safePred :: SNat (Succ n) -> SNat n
| > safePred (SSucc n) = n
| > safePred SZero = contra
|
| (Seeing the code here, perhaps "impossible" is a better name.)
|
| The last clause of safePred is indeed impossible. GHC issues an error on
| the code above. If we remove the last line, GHC (rightly) does not issue
| a warning about an incomplete pattern match. But, as documented on Trac
| #3927, there are other places where GHC does issue a warning about
| missing impossible branches. With contra, we could fill out such pattern
| matches and suppress the warning.
|
| When I initially wrote up my "contra" idea, I was remembering a case
| where GHC did not issue a warning on an inconsistent pattern match. In
| the process of writing this email, I found that old case, and I realized
| that it was my fault, not GHC's. I had originally thought that GHC's
| "impossible code" identification feature was incomplete, but now perhaps
| I was wrong. If GHC can always detect impossible code, the "contra" idea
| is less appealing than it once was to me, though it would still solve
| Shachaf's problem.
|
| Does this clarify the idea?
|
| Richard
|
| On Apr 3, 2013, at 1:49 PM, Simon Peyton-Jones
| wrote:
|
| > What precisely is the proposal here? That "unreachable code" be a
| warning rather than an error?
| >
| > Would you care to make a ticket with a clear specification? Thanks!
| >
| > Simon
| >
| > | -Original Message-
| > | From: glasgow-haskell-users-boun...@haskell.org
| > | [mailto:glasgow-haskell- users-boun...@haskell.org] On Behalf Of
| > | Richard Eisenberg
| > | Sent: 24 March 2013 14:49
| > | To: Shachaf Ben-Kiki
| > | Cc: glasgow-haskell-users
| > | Subject: Re: Allowing (Char ~ Bool => Void)?
| >
Re: Allowing (Char ~ Bool => Void)?
On Apr 5, 2013, at 3:10 AM, Simon Peyton-Jones wrote:
>
> I suppose you could have a magic constraint INSOLUBLE, say, with
> contra :: INSOLUBLE => c
> which had the effect of suppressing any enclosing "impossible branch" failure
> error reports.
That's *exactly* what I meant -- sorry if I was unclear.
> It's not clear how far out it would go. What about
> safePred SZero = if ... then contra else True
> or
> safePred SZero = case .. of { ...some other GADT matching… }
>
I think to have a consistent system, we would have to allow these, too. That's
silly perhaps, but it's not dangerous and it wouldn't break anything. We could
even imagine a new language flag that suppresses the "impossible code" error,
and then it's up to the programmer to figure out what code is impossible and
what isn't.
> I can't say I'm enthusiastic here.
To be fair, neither am I. This was just one idea of a way to proceed. I'm happy
to consider this idea abandoned.
>
>
> I WOULD like someone to help beef up the pattern-match overlap detector in
> the desugarer. That would be really useful.
>
> Simon
>
>
> | -Original Message-
> | From: Richard Eisenberg [mailto:e...@cis.upenn.edu]
> | Sent: 03 April 2013 19:59
> | To: Simon Peyton-Jones
> | Cc: Shachaf Ben-Kiki; glasgow-haskell-users
> | Subject: Re: Allowing (Char ~ Bool => Void)?
> |
> | I would call this more of an idea than a proposal -- I'm not advocating
> | that it's necessarily the right thing, but one possible solution both to
> | Shachaf's original question and the problem of spurious warnings about
> | bogus case branches.
> |
> | The idea is to introduce some new keyword, which I've called "contra",
> | which has the type (a ~ b) => c, where a cannot unify with b (and c is
> | totally unconstrained). Currently, whenever such an equality (a ~ b) is
> | in the context, GHC issues an error and prevents any further code. This
> | is often good behavior of a compiler, to prevent people from writing
> | impossible code. However, Shachaf found a case where it would be nice to
> | have code that executes in an inconsistent context. And, if we had
> | contra, then we could just stick contra in any inconsistent pattern
> | matches, and there would be no need to fix the warnings about incomplete
> | pattern matches.
> |
> | For example:
> |
> | > data Nat = Zero | Succ Nat
> | > data SNat :: Nat -> * where
> | > SZero :: SNat Zero
> | > SSucc :: SNat n -> SNat (Succ n)
> | >
> | > safePred :: SNat (Succ n) -> SNat n
> | > safePred (SSucc n) = n
> | > safePred SZero = contra
> |
> | (Seeing the code here, perhaps "impossible" is a better name.)
> |
> | The last clause of safePred is indeed impossible. GHC issues an error on
> | the code above. If we remove the last line, GHC (rightly) does not issue
> | a warning about an incomplete pattern match. But, as documented on Trac
> | #3927, there are other places where GHC does issue a warning about
> | missing impossible branches. With contra, we could fill out such pattern
> | matches and suppress the warning.
> |
> | When I initially wrote up my "contra" idea, I was remembering a case
> | where GHC did not issue a warning on an inconsistent pattern match. In
> | the process of writing this email, I found that old case, and I realized
> | that it was my fault, not GHC's. I had originally thought that GHC's
> | "impossible code" identification feature was incomplete, but now perhaps
> | I was wrong. If GHC can always detect impossible code, the "contra" idea
> | is less appealing than it once was to me, though it would still solve
> | Shachaf's problem.
> |
> | Does this clarify the idea?
> |
> | Richard
> |
> | On Apr 3, 2013, at 1:49 PM, Simon Peyton-Jones
> | wrote:
> |
> | > What precisely is the proposal here? That "unreachable code" be a
> | warning rather than an error?
> | >
> | > Would you care to make a ticket with a clear specification? Thanks!
> | >
> | > Simon
> | >
> | > | -Original Message-
> | > | From: glasgow-haskell-users-boun...@haskell.org
> | > | [mailto:glasgow-haskell- users-boun...@haskell.org] On Behalf Of
> | > | Richard Eisenberg
> | > | Sent: 24 March 2013 14:49
> | > | To: Shachaf Ben-Kiki
> | > | Cc: glasgow-haskell-users
> | > | Subject: Re: Allowing (Char ~ Bool => Void)?
> | > |
> | > | Though I've never run into the problem Shachaf mentions, this
> | > | certainly seems useful. However
