1.1 KiB
1.1 KiB
Type Level
data Coercion (a :: k) (b :: k) where
Coercion :: forall (k :: BOX) (a :: k) (b :: k). Coercible a b => Coercion a b
coerceWith :: Coercion a b -> a -> b
Empty
data Void
absurd :: Void -> a
vacuous :: Functor f => f Void -> f a
Proxy
data Proxy (t :: k) = Proxy
Symbol
symbolVal :: KnownSymbol n => proxy n -> String
Example:
b :: String
b = symbolVal (Proxy :: Proxy "foo")
someSymbolVal :: String -> SomeSymbol
Example:
Nat
natVal :: KnownNat n => proxy n -> Integer
Example:
a :: Integer
a = natVal (Proxy :: Proxy 1)
someNatVal :: Integer -> Maybe SomeNat
Example:
Type Equality
(:~:) :: k -> k -> *
(==) :: k -> k -> Bool
sym :: a :~: b -> b :~: a
trans :: a :~: b -> b :~: c -> a :~: c
castWith :: a :~: b -> a -> b
gcastWith :: a :~: b -> ((a ~ b) => r) -> r