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

[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users