Re: Heterogeneous equality into base?

6 Jul 2017

      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
 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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries