Proposal: Rework Data.Type.Equality.==

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

Proposal: Rework Data.Type.Equality.==

David Feuer
The discussion has been going for nearly a month, but I've only really
gotten feedback from Richard and Ryan Scott (which was both positive
and useful). Based on that feedback, I'd like to make this an official
proposal and get some votes. Be it proposed that Data.Type.Equality
shall be redefined as follows:

type family (a :: k) == (b :: k) :: Bool where
  f a == g b = f == g && a == b
  a == a = 'True
  _ == _ = 'False

Unlike the previous definition:

1. (==) is a *closed* type family.
2. It works out of the box for types of all kinds, in a completely
uniform manner.
3. It is now safe to conclude in all cases that (a == b) ~ 'True
entails a ~ b, although GHC will not give us direct evidence of that.

Since all the ad hoc instances and special cases are gone, there will
be cases in which the previous definition will reduce and this one
will not, and vice versa. But there was no particular rhyme or reason
to the way it used to be, and I think that making everything simple
and uniform is worth the (likely minor) breakage.

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

Re: Proposal: Rework Data.Type.Equality.==

Andreas Abel-2
 > The discussion has been going for nearly a month, but I've only really
 > gotten feedback from Richard and Ryan Scott

I guess not so many use type equality in Haskell and, consequently, have
no opinion formed.

On 08.09.2017 01:35, David Feuer wrote:

> The discussion has been going for nearly a month, but I've only really
> gotten feedback from Richard and Ryan Scott (which was both positive
> and useful). Based on that feedback, I'd like to make this an official
> proposal and get some votes. Be it proposed that Data.Type.Equality
> shall be redefined as follows:
>
> type family (a :: k) == (b :: k) :: Bool where
>    f a == g b = f == g && a == b
>    a == a = 'True
>    _ == _ = 'False
>
> Unlike the previous definition:
>
> 1. (==) is a *closed* type family.
> 2. It works out of the box for types of all kinds, in a completely
> uniform manner.
> 3. It is now safe to conclude in all cases that (a == b) ~ 'True
> entails a ~ b, although GHC will not give us direct evidence of that.
>
> Since all the ad hoc instances and special cases are gone, there will
> be cases in which the previous definition will reduce and this one
> will not, and vice versa. But there was no particular rhyme or reason
> to the way it used to be, and I think that making everything simple
> and uniform is worth the (likely minor) breakage.
>
> David Feuer
> _______________________________________________
> Libraries mailing list
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>


--
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

[hidden email]
http://www.cse.chalmers.se/~abela/
_______________________________________________
Libraries mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries