Re: Heterogeneous equality into base?

Hi Ben, This discussion of heterogeneous equality in base may be of interest to you. Did you have to use a similar definition to get the new Typeable stuff working? I would imagine so. If you indeed did, that would provide a good argument for exporting this definition from base. Separately from seeking Ben's input, I am in favor of this addition. If (:~:) is in base, (:~~:) should be, too. Thanks, Richard

On Jul 6, 2017, at 6:10 PM, Wolfgang Jeltsch wrote:

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

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries