Version 4 (modified by 4 years ago) (diff) | ,
---|

# Naming issues in type-level programming modules

This page summarizes current type-level programming constructs in modules that ship with GHC. At the bottom is a list of open questions about good names for these operations.

## Module `Data.Type.Equality`

-- 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)

## Module `Data.Type.Coercion`

-- 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)

## Module `Data.Proxy`

data Proxy t = Proxy data KProxy (t :: *) = KProxy asProxyTypeOf :: a -> Proxy a -> a asProxyTypeOf = const

## Module `Data.Typeable`

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))

## Module `GHC.TypeLits`

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

## Module `GHC.Prim`

class Coercible a b where coerce :: a -> b

# Issues

These are in no particular order, but they are numbered for easy reference.

`EqualityT`

and`CoercionT`

sound like monad transformers. I (Richard) have actually been confused by this at one point.

- Should
`KProxy`

's data constructor be named`KProxy`

? Reusing the name here requires users to use a`'`

every time they want to use the promoted data constructor`KProxy`

.

- There are up to three different ways type-level 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);`(<=?)`

(Boolean-valued) vs.`(<=)`

(constraint); and`Coercible`

(constraint) vs.`Coercion`

(GADT).

`eqT`

(from`Data.Typeable`

) and`equalsT`

(from`Data.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.

- I propose the following, further addition to
`Data.Type.Equality`

:type family a == b where a == a = True a == b = False