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

[David Feuer]

(==), 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 at gmail.com>
wrote:

> On 10 August 2017 at 14:44, David Feuer <david.feuer at gmail.com> 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" <david.feuer at gmail.com> 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 at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> >
>
>
>
> --
> Ivan Lazar Miljenovic
> Ivan.Miljenovic at gmail.com
> http://IvanMiljenovic.wordpress.com
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20170810/37d28f87/attachment.html>