Copyright	(c) Justin Le 2016
License	MIT
Maintainer	justin@jle.im
Stability	unstable
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

GHC.TypeLits.Witnesses

Contents

Nats
Symbols

Description

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.

Synopsis

data SNat n = KnownNat n => SNat
data SomeNat where
- pattern SomeNat_ :: SNat n -> SomeNat
data Natural where
- pattern FromSNat :: SNat n -> Natural
fromSNat :: SNat n -> Natural
withKnownNat :: SNat n -> (KnownNat n => r) -> r
withSomeNat :: Natural -> (forall n. SNat n -> r) -> r
toSomeNat :: Natural -> SomeNat
(%+) :: SNat n -> SNat m -> SNat (n + m)
(%-) :: SNat n -> SNat m -> SNat (n - m)
minusSNat :: SNat n -> SNat m -> Either (CmpNat n m :~: 'LT) (SNat (n - m))
minusSNat_ :: SNat n -> SNat m -> Maybe (SNat (n - m))
(%*) :: SNat n -> SNat m -> SNat (n * m)
(%^) :: SNat n -> SNat m -> SNat (n ^ m)
(%<=?) :: SNat n -> SNat m -> n :<=? m
sCmpNat :: SNat n -> SNat m -> SCmpNat n m
unsafeLiftNatOp1 :: (Natural -> Natural) -> SNat n -> SNat m
unsafeLiftNatOp2 :: (Natural -> Natural -> Natural) -> SNat n -> SNat m -> SNat o
data SSymbol n = KnownSymbol n => SSymbol
data SomeSymbol where
- pattern SomeSymbol_ :: SSymbol n -> SomeSymbol
pattern FromSSymbol :: SSymbol n -> String
fromSSymbol :: SSymbol n -> String
withKnownSymbol :: SSymbol n -> (KnownSymbol n => r) -> r
withSomeSymbol :: String -> (forall n. SSymbol n -> r) -> r
toSomeSymbol :: String -> SomeSymbol

Nats

data SNat n Source #

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.

Constructors

KnownNat n => SNat

Instances

Instances details

TestEquality SNat Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b) #
GCompare SNat Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods gcompare :: forall (a :: k) (b :: k). SNat a -> SNat b -> GOrdering a b #
GEq SNat Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods geq :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b) #
GShow SNat Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods gshowsPrec :: forall (a :: k). Int -> SNat a -> ShowS #
Show (SNat n) Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods showsPrec :: Int -> SNat n -> ShowS # show :: SNat n -> String # showList :: [SNat n] -> ShowS #
Eq (SNat n) Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods (==) :: SNat n -> SNat n -> Bool # (/=) :: SNat n -> SNat n -> Bool #
Ord (SNat n) Source #
Instance details 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

Instances details

Read SomeNat	Since: base-4.7.0.0
Instance details 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
Instance details Defined in GHC.TypeNats Methods showsPrec :: Int -> SomeNat -> ShowS # show :: SomeNat -> String # showList :: [SomeNat] -> ShowS #
Eq SomeNat	Since: base-4.7.0.0
Instance details Defined in GHC.TypeNats Methods (==) :: SomeNat -> SomeNat -> Bool # (/=) :: SomeNat -> SomeNat -> Bool #
Ord SomeNat	Since: base-4.7.0.0
Instance details 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

Instances details

Enum Natural	Since: base-4.8.0.0
Instance details 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
Instance details 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
Instance details 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
Instance details 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
Instance details Defined in GHC.Real Methods toRational :: Natural -> Rational #
Show Natural	Since: base-4.8.0.0
Instance details Defined in GHC.Show Methods showsPrec :: Int -> Natural -> ShowS # show :: Natural -> String # showList :: [Natural] -> ShowS #
Eq Natural
Instance details Defined in GHC.Num.Natural Methods (==) :: Natural -> Natural -> Bool # (/=) :: Natural -> Natural -> Bool #
Ord Natural
Instance details 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 #
TestEquality SNat Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b) #
GCompare SNat Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods gcompare :: forall (a :: k) (b :: k). SNat a -> SNat b -> GOrdering a b #
GEq SNat Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods geq :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b) #
GShow SNat Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods gshowsPrec :: forall (a :: k). Int -> SNat a -> ShowS #
type Compare (a :: Natural) (b :: Natural)
Instance details Defined in Data.Type.Ord type Compare (a :: Natural) (b :: Natural) = CmpNat a b

fromSNat :: SNat n -> Natural Source #

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

This stands in the singletons fromSing function.

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

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 Source #

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 Source #

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

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

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

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

A version of minusSNat that just returns a Maybe.

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

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

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 Source #

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

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

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

Unsafe

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

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 Source #

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 Source #

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.

Constructors

KnownSymbol n => SSymbol

Instances

Instances details

TestEquality SSymbol Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods testEquality :: forall (a :: k) (b :: k). SSymbol a -> SSymbol b -> Maybe (a :~: b) #
GCompare SSymbol Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods gcompare :: forall (a :: k) (b :: k). SSymbol a -> SSymbol b -> GOrdering a b #
GEq SSymbol Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods geq :: forall (a :: k) (b :: k). SSymbol a -> SSymbol b -> Maybe (a :~: b) #
GShow SSymbol Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods gshowsPrec :: forall (a :: k). Int -> SSymbol a -> ShowS #
Show (SSymbol n) Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods showsPrec :: Int -> SSymbol n -> ShowS # show :: SSymbol n -> String # showList :: [SSymbol n] -> ShowS #
Eq (SSymbol n) Source #
Instance details Defined in GHC.TypeLits.Witnesses Methods (==) :: SSymbol n -> SSymbol n -> Bool # (/=) :: SSymbol n -> SSymbol n -> Bool #
Ord (SSymbol n) Source #
Instance details 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

Instances details

Read SomeSymbol	Since: base-4.7.0.0
Instance details 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
Instance details Defined in GHC.TypeLits Methods showsPrec :: Int -> SomeSymbol -> ShowS # show :: SomeSymbol -> String # showList :: [SomeSymbol] -> ShowS #
Eq SomeSymbol	Since: base-4.7.0.0
Instance details Defined in GHC.TypeLits Methods (==) :: SomeSymbol -> SomeSymbol -> Bool # (/=) :: SomeSymbol -> SomeSymbol -> Bool #
Ord SomeSymbol	Since: base-4.7.0.0
Instance details 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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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.