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

[David Feuer]

You can see the two main approaches in
https://phabricator.haskell.org/D3835 and
https://phabricator.haskell.org/D3837

On Thu, Aug 10, 2017 at 1:57 AM, David Feuer <david.feuer at gmail.com> wrote:
> 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