Naming issues in typelevel programming modules
This page summarizes current typelevel programming constructs in modules that ship with GHC. At the bottom is a list of open questions about good names for these operations.
Data.Type.Equality
Module  Reified equality
data a :~: b where
Refl :: a :~: a
sym :: (a :~: b) > (b :~: a)
trans :: (a :~: b) > (b :~: c) > (a :~: c)
castWith :: (a :~: b) > a > b
liftEq :: (a :~: b) > (f a :~: f b)
liftEq2 :: (a :~: a') > (b :~: b') > (f a b :~: f a' b')
liftEq3 :: (a :~: a') > (b :~: b') > (c :~: c') > (f a b c :~: f a' b' c')
liftEq4 :: (a :~: a') > (b :~: b') > (c :~: c') > (d :~: d')
> (f a b c d :~: f a' b' c' d')
lower :: (f a :~: f b) > a :~: b
class EqualityT f where
equalsT :: f a > f b > Maybe (a :~: b)
type family a == b where
a == a = True
a == b = False
Data.Type.Coercion
Module  Reified representational equality
data Coercion a b where
Coercion :: Coercible a b => Coercion a b
coerceWith :: Coercion a b > a > b
sym :: forall a b. Coercion a b > Coercion b a
trans :: Coercion a b > Coercion b c > Coercion a c
class CoercionT f where
coercionT :: f a > f b > Maybe (Coercion a b)
Data.Proxy
Module data Proxy t = Proxy
data KProxy (t :: *) = KProxy
asProxyTypeOf :: a > Proxy a > a
asProxyTypeOf = const
Data.Typeable
Module cast :: forall a b. (Typeable a, Typeable b) => a > Maybe b
eqT :: forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
gcast :: forall a b c. (Typeable a, Typeable b) => c a > Maybe (c b)
gcast1 :: forall c t t' a. (Typeable t, Typeable t')
=> c (t a) > Maybe (c (t' a))
gcast2 :: forall c t t' a b. (Typeable t, Typeable t')
=> c (t a b) > Maybe (c (t' a b))
GHC.TypeLits
Module data Nat
data Symbol
class KnownNat (n :: Nat) where
natSing :: SNat n
class KnownSymbol (n :: Symbol) where
symbolSing :: SSymbol n
natVal :: forall n proxy. KnownNat n => proxy n > Integer
symbolVal :: forall n proxy. KnownSymbol n => proxy n > String
data SomeNat = forall n. KnownNat n => SomeNat (Proxy n)
data SomeSymbol = forall n. KnownSymbol n => SomeSymbol (Proxy n)
someNatVal :: Integer > Maybe SomeNat  partial because of negative Ints
someSymbolVal :: String > SomeSymbol
infix 4 <=?, <=
infixl 6 +, 
infixl 7 *
infixr 8 ^
type x <= y = (x <=? y) ~ True  Note: in Constraint
type family (m :: Nat) <=? (n :: Nat) :: Bool
type family (m :: Nat) + (n :: Nat) :: Nat
type family (m :: Nat) * (n :: Nat) :: Nat
type family (m :: Nat) ^ (n :: Nat) :: Nat
type family (m :: Nat)  (n :: Nat) :: Nat
GHC.Prim
Module class Coercible a b where
coerce :: a > b
Issues
These are in no particular order, but they are numbered for easy reference.

EqualityT
andCoercionT
sound like monad transformers. I (Richard) have actually been confused by this at one point. 
Should
KProxy
's data constructor be namedKProxy
? Reusing the name here requires users to use a'
every time they want to use the promoted data constructorKProxy
. 
There are up to three different ways typelevel predicates can be defined: as Constraints, as GADTs wrapping constraints, or as type families returning
Bool
s. Is there a common naming convention among these? Right now, we have(~)
(constraint) vs(:~:)
(GADT);(<=?)
(Booleanvalued) vs.(<=)
(constraint); andCoercible
(constraint) vs.Coercion
(GADT). 
eqT
(fromData.Typeable
) andequalsT
(fromData.Type.Equality
) have similar names, achieve similar functions, but are subtly different. This may or may not be confusing. 
I (Richard) want to add the following function to
Data.Type.Equality
:
gcastWith :: (a :~: b) > ((a ~ b) => r) > r
gcastWith Refl x = x
I've tested this function in a real setting, and it (that is, type inference for it) works great.