GHC.TypeLits.Witnesses

This module essentially provides a lightweight subset of the singletons library specifically for Nat and Symbol, from GHC.TypeLits.

Its main functionality is for first-class manipulation of KnownNat and KnownSymbol constraints. For example, in general, if you have KnownNat n, GHC can't infer KnownNat (n + 1). And, if you have both KnownNat n and KnownNat m, GHC can't infer 'KnownNat (n + m).

This can be annoying when dealing with libraries and applications where one regularly adds and subtracts type-level nats and expects KnownNat instances to follow. For example, vector concatenation of length-encoded vector types can be:

concat :: (KnownNat n, KnownNat m) => Vector n a -> Vector m a -> Vector (n + m) a

But, now n + m does not have a KnownNat instance...which makes operations like this much less useful.

Usually, the easiest way to get around this is to use a typechecker plugin, like https://hackage.haskell.org/package/ghc-typelits-knownnat. However, we can do this without the help of a typechecker plugin using first-class values, at the cost of some increased verbosity.

We introduce SNat n, which is a term-level witness of knownnat-ness that can be manipulated as a first-class value.

If we have KnownNat n, we can construct an SNat n:

SNat :: KnownNat n -> SNat n

Furthermore, if we have an SNat n, we can pattern match on the SNat constructor to get a KnownNat n constraint:

myFunc :: SNat n -> Bool
myFunc SNat = ...  -- in this body, we have `KnownNat n`

So if we have KnownNat n and KnownNat m, we can get KnownNat (n + m) by using %+, which adds together SNats:

case (SNat :: SNat n) %+ (SNat :: SNat m) of
  SNat -> -- in this branch, we have `KnownNat (n + m)`

Note that this module converts between SNat and Natural, and not SNat and Integer, in GHC.TypeNats-style.

Of course, all of this functionality is provided by the singletons library, in Data.Singletons.TypeLits. This module can be useful if you want a lightweight alternative without the full might of singletons. The main benefit of the singletons library is providing a unified interface for singletons of all different kinds/types, and not just Natural and String.

Nats

data SNat n

An SNat n is a witness for KnownNat n.

This means that if you pattern match on the SNat constructor, in that branch you will have a KnownNat n constraint.

myFunc :: SNat n -> Bool
myFunc SNat = ...  -- in this body, we have `KnownNat n`

This is essentially a singleton for Nat, and stands in for the singletons SNat and Sing types.

Note that this type exists in base as of base 4.18.0 (GHC 9.6)

Constructors

KnownNat n => SNat

Instances

TestEquality SNat

Defined in GHC.TypeLits.Witnesses

Methods

testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b)

GCompare SNat

Defined in GHC.TypeLits.Witnesses

Methods

gcompare :: forall (a :: k) (b :: k). SNat a -> SNat b -> GOrdering a b

GEq SNat

Defined in GHC.TypeLits.Witnesses

Methods

geq :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b)

GShow SNat

Defined in GHC.TypeLits.Witnesses

Methods

gshowsPrec :: forall (a :: k). Int -> SNat a -> ShowS

Show (SNat n)

Defined in GHC.TypeLits.Witnesses

Methods

showsPrec :: Int -> SNat n -> ShowS

show :: SNat n -> String

showList :: [SNat n] -> ShowS

Eq (SNat n)

Defined in GHC.TypeLits.Witnesses

Methods

(==) :: SNat n -> SNat n -> Bool

(/=) :: SNat n -> SNat n -> Bool

Ord (SNat n)

Defined in GHC.TypeLits.Witnesses

Methods

compare :: SNat n -> SNat n -> Ordering

(<) :: SNat n -> SNat n -> Bool

(<=) :: SNat n -> SNat n -> Bool

(>) :: SNat n -> SNat n -> Bool

(>=) :: SNat n -> SNat n -> Bool

max :: SNat n -> SNat n -> SNat n

min :: SNat n -> SNat n -> SNat n

data SomeNat where

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Bundled Patterns

pattern SomeNat_ :: SNat n -> SomeNat

A useful pattern synonym for matching on a SomeNat as if it contained an SNat n, and not a Proxy n as it exists in GHC.TypeLits.

A layer of compatibility letting us use the original SomeNat type in a way that works well with SNat.

This stands in for the singletons SomeSing constructor.

Instances

Read SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

readsPrec :: Int -> ReadS SomeNat

readList :: ReadS [SomeNat]

readPrec :: ReadPrec SomeNat

readListPrec :: ReadPrec [SomeNat]

Show SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

showsPrec :: Int -> SomeNat -> ShowS

show :: SomeNat -> String

showList :: [SomeNat] -> ShowS

Eq SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

(==) :: SomeNat -> SomeNat -> Bool

(/=) :: SomeNat -> SomeNat -> Bool

Ord SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

compare :: SomeNat -> SomeNat -> Ordering

(<) :: SomeNat -> SomeNat -> Bool

(<=) :: SomeNat -> SomeNat -> Bool

(>) :: SomeNat -> SomeNat -> Bool

(>=) :: SomeNat -> SomeNat -> Bool

max :: SomeNat -> SomeNat -> SomeNat

min :: SomeNat -> SomeNat -> SomeNat

data Natural where

Natural number

Invariant: numbers <= 0xffffffffffffffff use the NS constructor

Bundled Patterns

pattern FromSNat :: SNat n -> Natural

A useful pattern synonym for matching on a Natural as if it "were" a SNat:

myFunc :: Natural -> Bool
myFunc (FromSNat x) = ...  -- x is `SNat n`, with n coming from the input

It can be used as a function, as well, to convert an SNat n back into the Natural that it represents.

This stands in for the singletons FromSing pattern synonym.

Instances

Data Natural

Since: base-4.8.0.0

Defined in Data.Data

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Natural -> c Natural

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Natural

toConstr :: Natural -> Constr

dataTypeOf :: Natural -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Natural)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Natural)

gmapT :: (forall b. Data b => b -> b) -> Natural -> Natural

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Natural -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Natural -> r

gmapQ :: (forall d. Data d => d -> u) -> Natural -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Natural -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Natural -> m Natural

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Natural -> m Natural

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Natural -> m Natural

Enum Natural

Since: base-4.8.0.0

Defined in GHC.Enum

Methods

succ :: Natural -> Natural

pred :: Natural -> Natural

toEnum :: Int -> Natural

fromEnum :: Natural -> Int

enumFrom :: Natural -> [Natural]

enumFromThen :: Natural -> Natural -> [Natural]

enumFromTo :: Natural -> Natural -> [Natural]

enumFromThenTo :: Natural -> Natural -> Natural -> [Natural]

Num Natural

Note that Natural's Num instance isn't a ring: no element but 0 has an additive inverse. It is a semiring though.

Since: base-4.8.0.0

Defined in GHC.Num

Methods

(+) :: Natural -> Natural -> Natural

(-) :: Natural -> Natural -> Natural

(*) :: Natural -> Natural -> Natural

negate :: Natural -> Natural

abs :: Natural -> Natural

signum :: Natural -> Natural

fromInteger :: Integer -> Natural

Read Natural

Since: base-4.8.0.0

Defined in GHC.Read

Methods

readsPrec :: Int -> ReadS Natural

readList :: ReadS [Natural]

readPrec :: ReadPrec Natural

readListPrec :: ReadPrec [Natural]

Integral Natural

Since: base-4.8.0.0

Defined in GHC.Real

Methods

quot :: Natural -> Natural -> Natural

rem :: Natural -> Natural -> Natural

div :: Natural -> Natural -> Natural

mod :: Natural -> Natural -> Natural

quotRem :: Natural -> Natural -> (Natural, Natural)

divMod :: Natural -> Natural -> (Natural, Natural)

toInteger :: Natural -> Integer

Real Natural

Since: base-4.8.0.0

Defined in GHC.Real

Methods

toRational :: Natural -> Rational

Show Natural

Since: base-4.8.0.0

Defined in GHC.Show

Methods

showsPrec :: Int -> Natural -> ShowS

show :: Natural -> String

showList :: [Natural] -> ShowS

Eq Natural

Defined in GHC.Num.Natural

Methods

(==) :: Natural -> Natural -> Bool

(/=) :: Natural -> Natural -> Bool

Ord Natural

Defined in GHC.Num.Natural

Methods

compare :: Natural -> Natural -> Ordering

(<) :: Natural -> Natural -> Bool

(<=) :: Natural -> Natural -> Bool

(>) :: Natural -> Natural -> Bool

(>=) :: Natural -> Natural -> Bool

max :: Natural -> Natural -> Natural

min :: Natural -> Natural -> Natural

TestCoercion SNat

Since: base-4.18.0.0

Defined in GHC.TypeNats

Methods

testCoercion :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (Coercion a b)

TestEquality SNat

Since: base-4.18.0.0

Defined in GHC.TypeNats

Methods

testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b)

TestEquality SNat

Defined in GHC.TypeLits.Witnesses

Methods

testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b)

GCompare SNat

Defined in Data.GADT.Internal

Methods

gcompare :: forall (a :: k) (b :: k). SNat a -> SNat b -> GOrdering a b

GCompare SNat

Defined in GHC.TypeLits.Witnesses

Methods

gcompare :: forall (a :: k) (b :: k). SNat a -> SNat b -> GOrdering a b

GEq SNat

Defined in Data.GADT.Internal

Methods

geq :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b)

GEq SNat

Defined in GHC.TypeLits.Witnesses

Methods

geq :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b)

GShow SNat

Defined in Data.GADT.Internal

Methods

gshowsPrec :: forall (a :: k). Int -> SNat a -> ShowS

GShow SNat

Defined in GHC.TypeLits.Witnesses

Methods

gshowsPrec :: forall (a :: k). Int -> SNat a -> ShowS

type Compare (a :: Natural) (b :: Natural)

Defined in Data.Type.Ord

type Compare (a :: Natural) (b :: Natural) = CmpNat a b

fromSNat :: SNat n -> Natural

Convert ("reflect") an SNat back into the Natural it represents.

This stands in the singletons fromSing function.

withKnownNat :: SNat n -> (KnownNat n => r) -> r

Given an SNat n and a value that would require a KnownNat n instance, create that value.

This stands in for the function of the same name from Data.Singletons.TypeLits.

withSomeNat :: Natural -> (forall n. SNat n -> r) -> r

Promote ("reify") a Natural to an SNat n, by providing a continuation that would handle it in a way that is polymorphic over all possible n.

This stands in the singletons withSomeSing function.

toSomeNat :: Natural -> SomeNat

Promote ("reify") a Natural to an SNat n existentially hidden inside a SomeNat. To use it, pattern match using SomeNat_.

This stands in the singletons toSomeSing function.

Operations

(%+) :: SNat n -> SNat m -> SNat (n + m)

Addition of SNats.

This also will provide the correct KnownNat instance for SNat (n + m), so can be used as a way to "add" KnownNat instances.

This stands in for the function with the same name from Data.Singletons.Prelude.Num.

(%-) :: SNat n -> SNat m -> SNat (n - m)

Subtraction of SNats. Note that this is unsafe, as will trigger a run-time underflow if m is bigger than n even though it will always succeed at compiletime.

This also will provide the correct KnownNat instance for SNat (n - m), so can be used as a way to "subtract" KnownNat instances.

This stands in for the function with the same name from Data.Singletons.Prelude.Num.

minusSNat :: SNat n -> SNat m -> Either (CmpNat n m :~: 'LT) (SNat (n - m))

A safe version of %-: it will return Left if n is less than m (with a witness that it is), or else return the subtracted SNat in Right in a way that is guarunteed to not have runtime underflow.

minusSNat_ :: SNat n -> SNat m -> Maybe (SNat (n - m))

A version of minusSNat that just returns a Maybe.

(%*) :: SNat n -> SNat m -> SNat (n * m)

Multiplication of SNats.

This also will provide the correct KnownNat instance for SNat (n * m), so can be used as a way to "multiply" KnownNat instances.

This stands in for the function with the same name from Data.Singletons.Prelude.Num.

(%^) :: SNat n -> SNat m -> SNat (n ^ m)

Exponentiation of SNats.

This also will provide the correct KnownNat instance for SNat (n ^ m), so can be used as a way to "exponentiate" KnownNat instances.

This stands in for the function with the same name from Data.Singletons.TypeLits.

Compare

(%<=?) :: SNat n -> SNat m -> n :<=? m

Compare n and m, categorizing them into one of the constructors of :<=?.

sCmpNat :: SNat n -> SNat m -> SCmpNat n m

Compare n and m, categorizing them into one of the constructors of SCmpNat.

Unsafe

unsafeLiftNatOp1 :: (Natural -> Natural) -> SNat n -> SNat m

Lift a unary operation to act on an SNat n that returns an SNat m. The function given must properly describe the relationship between n and m.

For example:

double :: SNat n -> SNat (n * 2)
double = unsafeLiftNatOp1 (*2)

The correctness of the relationship is not checked, so be aware that this can cause programs to break.

unsafeLiftNatOp2 :: (Natural -> Natural -> Natural) -> SNat n -> SNat m -> SNat o

Lift a binary operation to act on an SNat n and SNat m that returns an SNat o. The function given must properly describe the relationship between n, m, and o.

For example:

multiply :: SNat n -> SNat m -> SNat (n * m)
multiply = unsafeLiftNatOp2 (*)

The correctness of the relationship is not checked, so be aware that this can cause programs to break.

Symbols

data SSymbol n

An SSymbol n is a witness for KnownSymbol n.

This means that if you pattern match on the SSymbol constructor, in that branch you will have a KnownSymbol n constraint.

myFunc :: SSymbol n -> Bool
myFunc SSymbol = ...  -- in this body, we have `KnownSymbol n`

This is essentially a singleton for Symbol, and stands in for the singletons SSymbol and Sing types.

Note that this type exists in base as of base 4.18.0 (GHC 9.6)

Constructors

KnownSymbol n => SSymbol

Instances

TestEquality SSymbol

Defined in GHC.TypeLits.Witnesses

Methods

testEquality :: forall (a :: k) (b :: k). SSymbol a -> SSymbol b -> Maybe (a :~: b)

GCompare SSymbol

Defined in GHC.TypeLits.Witnesses

Methods

gcompare :: forall (a :: k) (b :: k). SSymbol a -> SSymbol b -> GOrdering a b

GEq SSymbol

Defined in GHC.TypeLits.Witnesses

Methods

geq :: forall (a :: k) (b :: k). SSymbol a -> SSymbol b -> Maybe (a :~: b)

GShow SSymbol

Defined in GHC.TypeLits.Witnesses

Methods

gshowsPrec :: forall (a :: k). Int -> SSymbol a -> ShowS

Show (SSymbol n)

Defined in GHC.TypeLits.Witnesses

Methods

showsPrec :: Int -> SSymbol n -> ShowS

show :: SSymbol n -> String

showList :: [SSymbol n] -> ShowS

Eq (SSymbol n)

Defined in GHC.TypeLits.Witnesses

Methods

(==) :: SSymbol n -> SSymbol n -> Bool

(/=) :: SSymbol n -> SSymbol n -> Bool

Ord (SSymbol n)

Defined in GHC.TypeLits.Witnesses

Methods

compare :: SSymbol n -> SSymbol n -> Ordering

(<) :: SSymbol n -> SSymbol n -> Bool

(<=) :: SSymbol n -> SSymbol n -> Bool

(>) :: SSymbol n -> SSymbol n -> Bool

(>=) :: SSymbol n -> SSymbol n -> Bool

max :: SSymbol n -> SSymbol n -> SSymbol n

min :: SSymbol n -> SSymbol n -> SSymbol n

data SomeSymbol where

This type represents unknown type-level symbols.

Bundled Patterns

pattern SomeSymbol_ :: SSymbol n -> SomeSymbol

A useful pattern synonym for matching on a SomeSymbol as if it contained an SSymbol n, and not a Proxy n as it exists in GHC.TypeLits.

A layer of compatibility letting us use the original SomeSymbol type in a way that works well with SSymbol.

This stands in for the singletons SomeSing constructor.

Instances

Read SomeSymbol

Since: base-4.7.0.0

Defined in GHC.TypeLits

Methods

readsPrec :: Int -> ReadS SomeSymbol

readList :: ReadS [SomeSymbol]

readPrec :: ReadPrec SomeSymbol

readListPrec :: ReadPrec [SomeSymbol]

Show SomeSymbol

Since: base-4.7.0.0

Defined in GHC.TypeLits

Methods

showsPrec :: Int -> SomeSymbol -> ShowS

show :: SomeSymbol -> String

showList :: [SomeSymbol] -> ShowS

Eq SomeSymbol

Since: base-4.7.0.0

Defined in GHC.TypeLits

Methods

(==) :: SomeSymbol -> SomeSymbol -> Bool

(/=) :: SomeSymbol -> SomeSymbol -> Bool

Ord SomeSymbol

Since: base-4.7.0.0

Defined in GHC.TypeLits

Methods

compare :: SomeSymbol -> SomeSymbol -> Ordering

(<) :: SomeSymbol -> SomeSymbol -> Bool

(<=) :: SomeSymbol -> SomeSymbol -> Bool

(>) :: SomeSymbol -> SomeSymbol -> Bool

(>=) :: SomeSymbol -> SomeSymbol -> Bool

max :: SomeSymbol -> SomeSymbol -> SomeSymbol

min :: SomeSymbol -> SomeSymbol -> SomeSymbol

pattern FromSSymbol :: SSymbol n -> String

A useful pattern synonym for matching on a String as if it "were" a SSymbol:

myFunc :: String -> Bool
myFunc (FromSSymbol x) = ...  -- x is `SSymbol n`, with n coming from the input

It can be used as a function, as well, to convert an SSymbol n back into the String that it represents.

This stands in for the singletons FromSing pattern synonym, except it matches on a String instead of a Text.

fromSSymbol :: SSymbol n -> String

Convert ("reflect") an SSymbol back into the String it represents.

This stands in the singletons fromSing function, except it returns a String instead of Text.

withKnownSymbol :: SSymbol n -> (KnownSymbol n => r) -> r

Given an SSymbol n and a value that would require a KnownSymbol n instance, create that value.

This stands in for the function of the same name from Data.Singletons.TypeLits.

withSomeSymbol :: String -> (forall n. SSymbol n -> r) -> r

Promote ("reify") a String to an SSymbol n, by providing a continuation that would handle it in a way that is polymorphic over all possible n.

This stands in the singletons withSomeSing function, except it takes a String instead of Text.

toSomeSymbol :: String -> SomeSymbol

Promote ("reify") a String to an SSymbol n existentially hidden inside a SomeNat. To use it, pattern match using SomeSymbol_.

This stands in the singletons toSomeSing function, except it takes a String instead of Text.