Let's rework Data.Type.Equality.==
David Feuer
david.feuer at gmail.com
Thu Aug 10 04:29:27 UTC 2017
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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170810/cb40e7a1/attachment.html>
More information about the Libraries
mailing list