September 2017 - Libraries

Proposal: Rework Data.Type.Equality.==
by David Feuer 08 Sep '17

08 Sep '17

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

2 1

Re: Let's rework Data.Type.Equality.==
by Ryan Scott 05 Sep '17

05 Sep '17

Personally, I'd be more inclined towards latter approach (in https://phabricator.haskell.org/D3837) After all, one of the key properties of (==) (for which the Haddocks even make a special note) is that it does not attempt to provide an instance that works for every possible kind. Indeed, as you've discovered, there are cases when it doesn't make sense to use DefaultEq, such as for (). I'll tentatively give my support for D3837, although I'd be curious to hear what Richard has to say about this (since I'm reasonably confident he gave (==) its current implementation). Ryan S.

5 8

Let's rework Data.Type.Equality.==
by David Feuer 01 Sep '17

01 Sep '17

The (==) type family in Data.Type.Equality was designed largely to calculate structural equality of types. However, limitations of GHC's type system at the type prevented this from being fully realized. Today, with TypeInType, we can actually do it, replacing the boatload of ad hoc instances like so: type (a :: k) == (b :: k) = Equal k a b infix 4 == type family Equal (k :: Type) (a :: k) (b :: k) where Equal k ((f :: j -> k) (a :: j)) ((g :: j -> k) (b :: j)) = Equal (j -> k) f g && Equal j a b Equal k a a = 'True Equal k a b = 'False This == behaves in a much more uniform way than the current one. I see two potential causes for complaint: 1. For types of kind *, the new version will sometimes fail to reduce when the old one succeeded (and vice versa). For example, GHC currently accepts eqeq :: forall (a :: *). proxy a -> (a == a) :~: 'True eqeq _ = Refl while the proposed version does not. 2. Some users may want non-structural equality on their types for some reason. The only example in base is type instance (a :: ()) == (b :: ()) = 'True which consists two types of kind () the same even if they're stuck types. But perhaps someone wants to implement a non-trivial type-level data structure with a special notion of equality. I don't think (1) is really worth worrying too much about. For (2), if users want to have control, we could at least use a mechanism similar to the above to make the obvious instances easier to write.

2 6