A library of combinators for dealing with heterogeneous equality

Heterogeneous.hs

{-# LANGUAGE CPP #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module {-Data.Type.Equality.-}Heterogeneous (
  -- * The heterogeneous equality types
  (:~~:)(..), type (~~),

  -- * Working with heterogeneous equality
  hSym, hTrans, hCastWith, hGcastWith, hApply, hInner, hOuter,

  -- * Boolean type-level heterogeneous equality
  type (===),

  -- * Conversion to and from homogenous equality
  fromHomogeneous, toHomogeneous
  ) where

#if MIN_VERSION_base(4,10,0)
import Data.Type.Equality ((:~~:)(..))
#endif
import Data.Type.Equality ((:~:)(..), type (~~), type (==))
import Data.Kind (Type)

#if !(MIN_VERSION_base(4,10,0))
-- | Kind heterogeneous propositional equality. Like '(:~:)', @a :~~: b@ is
-- inhabited by a terminating value if and only if @a@ is the same type as @b@.
data (:~~:) (a :: k1) :: forall (k2 :: Type). k2 -> Type where
-- data (a :: k1) :~~: (b :: k2) where
   HRefl :: a :~~: a
infix 4 :~~:
#endif

-- | Symmetry of heterogeneous equality
hSym :: (a :~~: b) -> (b :~~: a)
hSym HRefl = HRefl

-- | Transitivity of heterogenous equality
hTrans :: (a :~~: b) -> (b :~~: c) -> (a :~~: c)
hTrans HRefl HRefl = HRefl

-- | Type-safe cast, using propositional heterogeneous equality
hCastWith :: (a :~~: b) -> a -> b
hCastWith HRefl x = x

-- | Generalized form of type-safe cast using propositional
-- heterogeneous equality
hGcastWith :: (a :~~: b) -> ((a ~~ b) => r) -> r
hGcastWith HRefl x = x

-- | Apply one heterogeneous equality to another, respectively
hApply :: (f :~~: g) -> (a :~~: b) -> (f a :~~: g b)
hApply HRefl HRefl = HRefl

-- | Extract heterogeneous equality of the arguments from an equality of
-- applied types
hInner :: (f a :~~: g b) -> (a :~~: b)
hInner HRefl = HRefl

-- | Extract heterogeneous equality of type constructors from an equality of
-- applied types
hOuter :: (f a :~~: g b) -> (f :~~: g)
hOuter HRefl = HRefl

-- | A type family to compute Boolean heterogeneous equality. Instances are
-- provided only for /open/ kinds, such as @*@ and function kinds. Instances
-- are also provided for datatypes exported from base. A poly-kinded instance
-- is /not/ provided, as a recursive definition for algebraic kinds is
-- generally more useful.
type family (a :: k1) === (b :: k2) :: Bool where
  (a :: k) === (b :: k) = a == b
infix 4 ===

-- | Extract heterogeneous equality from homogeneous equality.
fromHomogeneous :: (a :~: b) -> (a :~~: b)
fromHomogeneous Refl = HRefl

-- | Extract homogeneous equality from heterogeneous equality.
toHomogeneous :: (a :~~: b) -> (a :~: b)
toHomogeneous HRefl = Refl