Re: Let's rework Data.Type.Equality.==

By the way.... the nicest version of the ad hoc equality would probably use a kind class: class TEq (k :: Type) where type (==) (a :: k) (b :: k) :: Bool type a == b = DefaultEq a b So then you could write instance TEq (Maybe k) instance TEq (Either j k) instance TEq [k] instance TEq (j -> k) instance TEq () where type _ == _ = 'True etc. On Aug 10, 2017 1:46 AM, "David Feuer" wrote:

(==), in that option, is an open type family, and Equal (more likely a synonym dealing with its kind) is a helper function. Note that Equality, in this version, calls == to deal with arguments.

type DefaultEq (a :: k) (b :: k) = Equal k a b

Then if con1 and con2 are constructors,

DefaultEq (con1 a b) (con2 c d) = (con1 exactly equals con2) && a == c && b == d

The == for the kinds of a/c and b/d could be anything a user wishes.

On Aug 10, 2017 1:35 AM, "Ivan Lazar Miljenovic" < ivan.miljenovic@gmail.com> wrote:

...

On 10 August 2017 at 14:44, David Feuer wrote:

...

To be more specific about the ad hoc equality option, I'm thinking about something like this (if it doesn't compile, I'm sure something similar will):

type family (a :: k) == (b :: k) :: Bool 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 && (a == b) Equal k a a = 'True Equal k a b = 'False

type instance (a :: Type) == b = Equal Type a b type instance (a :: Maybe k) == b = Equal Type a b

Since this is a closed type family, isn't doing any extra explicit type instances illegal?

...

....

So for example, we'd get

'Just (x :: k) == 'Just y = Equal (k -> Maybe k) 'Just && x == y = x == y

On Aug 10, 2017 12:29 AM, "David Feuer" wrote:

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.

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

-- Ivan Lazar Miljenovic Ivan.Miljenovic@gmail.com http://IvanMiljenovic.wordpress.com