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

[Ivan Lazar Miljenovic]

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