Heterogeneous equality
Wolfgang Jeltsch
wolfgang-it at jeltsch.info
Wed Jul 5 21:23:22 UTC 2017
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
More information about the Glasgow-haskell-users
mailing list