Heterogeneous equality into base?

[Wolfgang Jeltsch]

Hi!

Yes, I have some code that uses this heterogeneous equality type
apparently successfully. I will try to explain the idea behind this code
a bit.

There is a kind-polymorphic class Q that contains an associated type
synonym family that maps instances of Q to types of kind *. This type
synonym family shall be injective, and there should be actual witness of
this injectivity. This is achieved by requiring every instantiation of Q
to provide a heterogeneous equality proof of some kind. The equality
must be heterogeneous, because Q is kind-polymorphic.

Here is some code that illustrates the idea in more detail:

> {-# LANGUAGE GADTs,
>              PolyKinds,
>              TypeFamilies,
>              TypeOperators,
>              UndecidableInstances,
>              UndecidableSuperClasses #-}
> 
> import GHC.Exts (Constraint)
> 
> -- * Heterogeneous equality
> 
> data (a :: l) :~~: (b :: k) where
> 
>     Refl :: a :~~: a
> 
> transLike :: a :~~: c -> b :~~: c -> a :~~: b
> transLike Refl Refl = Refl
> 
> -- * Interface
> 
> type family C a :: k -> Constraint
> 
> class C (F q) q => Q q where
> 
>     type F q :: *
> 
>     eq :: (Q q', F q ~ F q') => q :~~: q'
> 
> -- * Implementation for []/Bool
> 
> class ListQ q where
> 
>     listEq :: q :~~: []
> 
> instance ListQ [] where
> 
>     listEq = Refl
> 
> type instance C Bool = ListQ
> 
> instance Q [] where
> 
>     type F [] = Bool
> 
>     eq = transLike listEq listEq

The central thing is the eq method, whose complete type is as follows:

    forall q q' . (Q q, Q q', F q ~ F q') => q :~~: q'

All the best,
Wolfgang

Am Donnerstag, den 06.07.2017, 17:15 -0400 schrieb David Menendez:
> Do you have any code examples that use heterogeneous equality? In the
> past, GHC has been less flexible with kind variables than with type
> variables, so I’m not sure what this would enable.
> 
> On Thu, Jul 6, 2017 at 4:45 PM, Wolfgang Jeltsch
> <wolfgang-it at jeltsch.info> wrote:
> > 
> > Hi!
> > 
> > The module Data.Type.Equality in the base package contains the type
> > (:~:) for homogeneous equality. However, a type for heterogeneous
> > equality would be very useful as well. I would define such a type as
> > follows:
> > 
> > > 
> > > {-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}
> > > 
> > > data (a :: k) :~~: (b :: l) where
> > > 
> > >     Refl :: a :~~: a
> > Is there already such a type in the base package? If not, does it
> > make
> > sense to file a feature request (or would such a proposal be likely
> > to
> > not being accepted for some reason)?
> > 
> > All the best,
> > Wolfgang
> > _______________________________________________
> > Libraries mailing list
> > Libraries at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> 
>