Re: Heterogeneous equality

[Richard Eisenberg]

> On Jul 5, 2017, at 5:23 PM, Wolfgang Jeltsch <wolfgang...@jeltsch.info> wrote:
> 
> Hi!
> 
> The base package contains the module Data.Type.Equality, which contains
> the type (:~:) for homogeneous equality. I was a bit surprised that
> there is no type for heterogeneous equality there. Is there such a type
> somewhere else in the standard library?

I don't believe it is, but (in my opinion) it should be.

> 
> I tried to define a type for heterogeneous equality myself as follows:
> 
>> {-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}
>> 
>> data a :~~: b where
>> 
>> HRefl :: a :~~: a
> 
> To my surprise, the kind of (:~~:) defined this way is k -> k -> *, not
> k -> l -> *. Why is this?

Because the definition of heterogeneous equality requires polymorphic 
recursion, in that the usage of (:~~:) in the type of HRefl has different kind 
indices than the declaration head. Polymorphic recursion is allowed only when 
you have a *complete user-supplied kind signature*, as documented here 
(https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#complete-user-supplied-kind-signatures-and-polymorphic-recursion).

This surprised me, too, when I first encountered it, but I believe it's the 
correct behavior.
Richard
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

Heterogeneous equality

[Wolfgang Jeltsch]

Hi!

The base package contains the module Data.Type.Equality, which contains
the type (:~:) for homogeneous equality. I was a bit surprised that
there is no type for heterogeneous equality there. Is there such a type
somewhere else in the standard library?

I tried to define a type for heterogeneous equality myself as follows:

> {-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}
> 
> data a :~~: b where
> 
> HRefl :: a :~~: a

To my surprise, the kind of (:~~:) defined this way is k -> k -> *, not
k -> l -> *. Why is this? Apparently, the latter, more general, kind is
possible, since we can define (:~~:) :: k -> l -> * as follows:

> {-# LANGUAGE GADTs, PolyKinds, TypeOperators #-}
> 
> data (a :: k) :~~: (b :: l) where
> 
> HRefl :: a :~~: a

All the best,
Wolfgang
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users