| Copyright | (c) 2018-2021 Iris Ward |
|---|---|
| License | BSD3 |
| Maintainer | aditu.venyhandottir@gmail.com |
| Stability | experimental |
| Safe Haskell | Safe |
| Language | Haskell2010 |
Data.TypeLits
Description
This module provides the same interface as GHC.TypeLits, but with
naming conflicts resolved in favour of this package. For example,
(<=) resolves to the kind-polymorphic version from Data.TypeNums.
If you are only working with type-level numbers, import Data.TypeNums instead. This module is purely for convenience for those who want to use both functionality from GHC.TypeLits and functionality from Data.TypeNums.
Synopsis
- data Nat
- class KnownNat (n :: Nat)
- natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Integer
- natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Integer
- data SomeNat = KnownNat n => SomeNat (Proxy n)
- someNatVal :: Integer -> Maybe SomeNat
- sameNat :: forall (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)
- data TInt
- class KnownInt (n :: k)
- intVal :: forall n proxy. KnownInt n => proxy n -> Integer
- intVal' :: forall n. KnownInt n => Proxy# n -> Integer
- data SomeInt = forall n.KnownInt n => SomeInt (Proxy n)
- someIntVal :: Integer -> SomeInt
- data Rat = forall k. k :% Nat
- class KnownRat r
- ratVal :: forall proxy r. KnownRat r => proxy r -> Rational
- ratVal' :: forall r. KnownRat r => Proxy# r -> Rational
- data SomeRat = forall r.KnownRat r => SomeRat (Proxy r)
- someRatVal :: Rational -> SomeRat
- type (==?) (a :: k) (b :: k) = (==) a b
- type (/=?) (a :: k) (b :: k) = Not ((==) a b)
- type family (a :: k1) <=? (b :: k2) :: Bool where ...
- type (==) (a :: k) (b :: k) = (==) a b ~ 'True
- type (/=) (a :: k) (b :: k) = (==) a b ~ 'False
- type (<=) (a :: k1) (b :: k2) = (a <=? b) ~ 'True
- type (<) (a :: k1) (b :: k2) = (b <=? a) ~ 'False
- type (>=) (a :: k1) (b :: k2) = (b <=? a) ~ 'True
- type (>) (a :: k1) (b :: k2) = (a <=? b) ~ 'False
- type (+) a b = Add a b
- type (-) a b = Sub a b
- type * a b = Mul a b
- type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
- data Symbol
- type family AppendSymbol (a :: Symbol) (b :: Symbol) :: Symbol where ...
- type family CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering where ...
- class KnownSymbol (n :: Symbol)
- symbolVal :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n -> String
- symbolVal' :: forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
- data SomeSymbol = KnownSymbol n => SomeSymbol (Proxy n)
- someSymbolVal :: String -> SomeSymbol
- sameSymbol :: forall (a :: Symbol) (b :: Symbol). (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Maybe (a :~: b)
- type family TypeError (a :: ErrorMessage) :: b where ...
- data ErrorMessage
Type level numbers
Naturals
(Kind) This is the kind of type-level natural numbers.
This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.
Since: base-4.7.0.0
Minimal complete definition
natSing
This type represents unknown type-level natural numbers.
Since: base-4.10.0.0
someNatVal :: Integer -> Maybe SomeNat #
Convert an integer into an unknown type-level natural.
Since: base-4.7.0.0
sameNat :: forall (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b) #
We either get evidence that this function was instantiated with the
same type-level numbers, or Nothing.
Since: base-4.7.0.0
Integers
(Kind) An integer that may be negative.
class KnownInt (n :: k) Source #
This class gives the (value-level) integer associated with a type-level
integer. There are instances of this class for every concrete natural:
0, 1, 2, etc. There are also instances of this class for every negated
natural, such as Neg 1
Minimal complete definition
intSing
intVal :: forall n proxy. KnownInt n => proxy n -> Integer Source #
Get the value associated with a type-level integer
This type represents unknown type-level integers.
Since: 0.1.1
someIntVal :: Integer -> SomeInt Source #
Convert an integer into an unknown type-level integer.
Since: 0.1.1
Rationals
Type constructor for a rational
Instances
This class gives the (value-level) rational associated with a type-level rational. There are instances of this class for every combination of a concrete integer and concrete natural.
Minimal complete definition
ratSing
Instances
| KnownInt n => KnownRat (n :: k) Source # | |
Defined in Data.TypeNums.Rats Methods ratSing :: SRat n | |
| (KnownInt n, KnownNat d, d /= 0) => KnownRat (n :% d :: Rat) Source # | |
Defined in Data.TypeNums.Rats | |
| (TypeError ('Text "Denominator must not equal 0") :: Constraint) => KnownRat (n :% 0 :: Rat) Source # | |
Defined in Data.TypeNums.Rats | |
ratVal :: forall proxy r. KnownRat r => proxy r -> Rational Source #
Get the value associated with a type-level rational
This type represents unknown type-level integers.
Since: 0.1.1
someRatVal :: Rational -> SomeRat Source #
Convert a rational into an unknown type-level rational.
Since: 0.1.1
Type level numerical operations
Comparison
type (==?) (a :: k) (b :: k) = (==) a b infix 4 Source #
Boolean type-level equals. Useful for e.g.
If (x ==? 0)
type family (a :: k1) <=? (b :: k2) :: Bool where ... infix 4 Source #
Boolean comparison of two type-level numbers
Equations
| (a :: Nat) <=? (b :: Nat) = (<=?) a b | |
| ('Pos a) <=? ('Pos b) = (<=?) a b | |
| ('Neg _) <=? ('Pos _) = 'True | |
| ('Pos 0) <=? ('Neg 0) = 'True | |
| ('Pos _) <=? ('Neg _) = 'False | |
| ('Pos a) <=? b = a <=? b | |
| a <=? ('Pos b) = a <=? b | |
| 0 <=? ('Neg 0) = 'True | |
| (a :: Nat) <=? ('Neg _) = 'False | |
| ('Neg a) <=? (b :: Nat) = 'True | |
| ('Neg a) <=? ('Neg b) = (<=?) b a | |
| (n :% 0) <=? _ = TypeError ('Text "Denominator must not equal 0") | |
| _ <=? (n :% 0) = TypeError ('Text "Denominator must not equal 0") | |
| (n1 :% d1) <=? (n2 :% d2) = (n1 * d2) <=? (n2 * d1) | |
| a <=? (n :% d) = (a * d) <=? n | |
| (n :% d) <=? b = n <=? (b * d) |
type (==) (a :: k) (b :: k) = (==) a b ~ 'True infix 4 Source #
Equality constraint, used as e.g. (x == 3) => _
Arithmetic
type * a b = Mul a b infixl 7 Source #
The product of two type-level numbers.
Due to changes in GHC 8.6, using this operator infix and unqualified requires the NoStarIsType language extension to be active. See the GHC 8.6.x migration guide for details: https://ghc.haskell.org/trac/ghc/wiki/Migration/8.6
type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 #
Exponentiation of type-level naturals.
Since: base-4.7.0.0
Symbols
type family AppendSymbol (a :: Symbol) (b :: Symbol) :: Symbol where ... #
Concatenation of type-level symbols.
Since: base-4.10.0.0
type family CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering where ... #
Comparison of type-level symbols, as a function.
Since: base-4.7.0.0
class KnownSymbol (n :: Symbol) #
This class gives the string associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.
Since: base-4.7.0.0
Minimal complete definition
symbolSing
symbolVal :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n -> String #
Since: base-4.7.0.0
symbolVal' :: forall (n :: Symbol). KnownSymbol n => Proxy# n -> String #
Since: base-4.8.0.0
data SomeSymbol #
This type represents unknown type-level symbols.
Constructors
| KnownSymbol n => SomeSymbol (Proxy n) | Since: base-4.7.0.0 |
Instances
| Eq SomeSymbol | Since: base-4.7.0.0 |
Defined in GHC.TypeLits | |
| 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 # | |
| 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 # | |
someSymbolVal :: String -> SomeSymbol #
Convert a string into an unknown type-level symbol.
Since: base-4.7.0.0
sameSymbol :: forall (a :: Symbol) (b :: Symbol). (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Maybe (a :~: b) #
We either get evidence that this function was instantiated with the
same type-level symbols, or Nothing.
Since: base-4.7.0.0
User-defined type errors
type family TypeError (a :: ErrorMessage) :: b where ... #
The type-level equivalent of error.
The polymorphic kind of this type allows it to be used in several settings. For instance, it can be used as a constraint, e.g. to provide a better error message for a non-existent instance,
-- in a context
instance TypeError (Text "Cannot Show functions." :$$:
Text "Perhaps there is a missing argument?")
=> Show (a -> b) where
showsPrec = error "unreachable"
It can also be placed on the right-hand side of a type-level function to provide an error for an invalid case,
type family ByteSize x where
ByteSize Word16 = 2
ByteSize Word8 = 1
ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:
Text " is not exportable.")
Since: base-4.9.0.0
data ErrorMessage #
A description of a custom type error.
Constructors
| Text Symbol | Show the text as is. |
| ShowType t | Pretty print the type.
|
| ErrorMessage :<>: ErrorMessage infixl 6 | Put two pieces of error message next to each other. |
| ErrorMessage :$$: ErrorMessage infixl 5 | Stack two pieces of error message on top of each other. |