Heterogeneous equality into base?

[Richard Eisenberg]

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 <wolfgang-it at jeltsch.info> 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
>> <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
>> 
>> 
> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries