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

[David Feuer]

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" <david.feuer at gmail.com> 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 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/dc86f176/attachment-0001.html>