Data.Parameterized.NatRepr

This defines a type NatRepr for representing a type-level natural at runtime. This can be used to branch on a type-level value. For each n, NatRepr n contains a single value containing the vlaue n. This can be used to help use type-level variables on code with data dependendent types.

The TestEquality instance for NatRepr is implemented using unsafeCoerce, as is the isZeroNat function. This should be typesafe because we maintain the invariant that the integer value contained in a NatRepr value matches its static type.

Documentation

data NatRepr (n :: Nat)

A runtime presentation of a type-level Nat.

This can be used for performing dynamic checks on a type-level natural numbers.

Instances

TestEquality NatRepr

Defined in Data.Parameterized.NatRepr

Methods

testEquality :: NatRepr a -> NatRepr b -> Maybe (a :~: b)

HashableF NatRepr

Defined in Data.Parameterized.NatRepr

Methods

hashWithSaltF :: Int -> NatRepr tp -> Int

hashF :: NatRepr tp -> Int

ShowF NatRepr

Defined in Data.Parameterized.NatRepr

Methods

withShow :: p NatRepr -> q tp -> (Show (NatRepr tp) -> a) -> a

showF :: NatRepr tp -> String

showsPrecF :: Int -> NatRepr tp -> String -> String

OrdF NatRepr

Defined in Data.Parameterized.NatRepr

Methods

compareF :: NatRepr x -> NatRepr y -> OrderingF x y

leqF :: NatRepr x -> NatRepr y -> Bool

ltF :: NatRepr x -> NatRepr y -> Bool

geqF :: NatRepr x -> NatRepr y -> Bool

gtF :: NatRepr x -> NatRepr y -> Bool

KnownNat n => KnownRepr NatRepr (n :: Nat)

Defined in Data.Parameterized.NatRepr

Methods

knownRepr :: NatRepr n

Eq (NatRepr m)

Defined in Data.Parameterized.NatRepr

Methods

(==) :: NatRepr m -> NatRepr m -> Bool

(/=) :: NatRepr m -> NatRepr m -> Bool

Show (NatRepr n)

Defined in Data.Parameterized.NatRepr

Methods

showsPrec :: Int -> NatRepr n -> ShowS

show :: NatRepr n -> String

showList :: [NatRepr n] -> ShowS

Hashable (NatRepr n)

Defined in Data.Parameterized.NatRepr

Methods

hashWithSalt :: Int -> NatRepr n -> Int

hash :: NatRepr n -> Int

PolyEq (NatRepr m) (NatRepr n)

Defined in Data.Parameterized.NatRepr

Methods

polyEqF :: NatRepr m -> NatRepr n -> Maybe (NatRepr m :~: NatRepr n)

polyEq :: NatRepr m -> NatRepr n -> Bool

natValue :: NatRepr n -> Integer

The underlying integer value of the number.

knownNat :: forall n. KnownNat n => NatRepr n

This generates a NatRepr from a type-level context.

withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r

Deprecated: This function is potentially unsafe and is schedueled to be removed.

data IsZeroNat n where

Constructors

ZeroNat :: IsZeroNat 0

NonZeroNat :: IsZeroNat (n + 1)

isZeroNat :: NatRepr n -> IsZeroNat n

data NatComparison m n where

Result of comparing two numbers.

Constructors

NatLT :: (x + 1) <= (x + (y + 1)) => !(NatRepr y) -> NatComparison x (x + (y + 1))

NatEQ :: NatComparison x x

NatGT :: (x + 1) <= (x + (y + 1)) => !(NatRepr y) -> NatComparison (x + (y + 1)) x

compareNat :: NatRepr m -> NatRepr n -> NatComparison m n

decNat :: 1 <= n => NatRepr n -> NatRepr (n - 1)

Decrement a NatRepr

predNat :: NatRepr (n + 1) -> NatRepr n

Get the predicessor of a nat

incNat :: NatRepr n -> NatRepr (n + 1)

Increment a NatRepr

addNat :: NatRepr m -> NatRepr n -> NatRepr (m + n)

subNat :: n <= m => NatRepr m -> NatRepr n -> NatRepr (m - n)

divNat :: 1 <= n => NatRepr (m * n) -> NatRepr n -> NatRepr m

halfNat :: NatRepr (n + n) -> NatRepr n

withDivModNat :: forall n m a. NatRepr n -> NatRepr m -> (forall div mod. n ~ ((div * m) + mod) => NatRepr div -> NatRepr mod -> a) -> a

natMultiply :: NatRepr n -> NatRepr m -> NatRepr (n * m)

someNat :: Integer -> Maybe (Some NatRepr)

maxNat :: NatRepr m -> NatRepr n -> Some NatRepr

Return the maximum of two nat representations.

natRec :: forall m f. NatRepr m -> f 0 -> (forall n. NatRepr n -> f n -> f (n + 1)) -> f m

Recursor for natural numbeers.

natForEach :: forall l h a. NatRepr l -> NatRepr h -> (forall n. (l <= n, n <= h) => NatRepr n -> a) -> [a]

Apply a function to each element in a range; return the list of values obtained.

data NatCases m n where

Constructors

NatCaseLT :: LeqProof (m + 1) n -> NatCases m n

NatCaseEQ :: NatCases m m

NatCaseGT :: LeqProof (n + 1) m -> NatCases m n

testNatCases :: forall m n. NatRepr m -> NatRepr n -> NatCases m n

Bitvector utilities

widthVal :: NatRepr n -> Int

Return the value of the nat representation.

minUnsigned :: NatRepr w -> Integer

Return minimum unsigned value for bitvector with given width (always 0).

maxUnsigned :: NatRepr w -> Integer

Return maximum unsigned value for bitvector with given width.

minSigned :: 1 <= w => NatRepr w -> Integer

Return minimum value for bitvector in 2s complement with given width.

maxSigned :: 1 <= w => NatRepr w -> Integer

Return maximum value for bitvector in 2s complement with given width.

toUnsigned :: NatRepr w -> Integer -> Integer

toUnsigned w i maps i to a i mod 2^w.

toSigned :: 1 <= w => NatRepr w -> Integer -> Integer

toSigned w i interprets the least-significant w bits in i as a signed number in two's complement notation and returns that value.

unsignedClamp :: NatRepr w -> Integer -> Integer

unsignedClamp w i rounds i to the nearest value between 0 and 2^w-1 (inclusive).

signedClamp :: 1 <= w => NatRepr w -> Integer -> Integer

signedClamp w i rounds i to the nearest value between -2^(w-1) and 2^(w-1)-1 (inclusive).

LeqProof

data LeqProof m n where

LeqProof m n is a type whose values are only inhabited when m is less than or equal to n.

Constructors

LeqProof :: m <= n => LeqProof m n

testLeq :: forall m n. NatRepr m -> NatRepr n -> Maybe (LeqProof m n)

x testLeq y checks whether x is less than or equal to y.

testStrictLeq :: forall m n. m <= n => NatRepr m -> NatRepr n -> Either (LeqProof (m + 1) n) (m :~: n)

leqRefl :: forall f n. f n -> LeqProof n n

Apply reflexivity to LeqProof

leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p

Apply transitivity to LeqProof

leqAdd2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)

Add both sides of two inequalities

leqSub2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)

Subtract sides of two inequalities.

leqMulCongr :: LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)

Congruence rule for multiplication

LeqProof combinators

leqProof :: m <= n => f m -> g n -> LeqProof m n

Create a leqProof using two proxies

withLeqProof :: LeqProof m n -> (m <= n => a) -> a

isPosNat :: NatRepr n -> Maybe (LeqProof 1 n)

Test whether natural number is positive.

leqAdd :: forall f m n p. LeqProof m n -> f p -> LeqProof m (n + p)

Produce proof that adding a value to the larger element in an LeqProof is larger

leqSub :: forall m n p. LeqProof m n -> LeqProof p m -> LeqProof (m - p) n

Produce proof that subtracting a value from the smaller element is smaller.

leqMulPos :: forall p q x y. (1 <= x, 1 <= y) => p x -> q y -> LeqProof 1 (x * y)

Multiplying two positive numbers results in a positive number.

leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)

addIsLeq :: f n -> g m -> LeqProof n (n + m)

withAddLeq :: forall n m a. NatRepr n -> NatRepr m -> (n <= (n + m) => NatRepr (n + m) -> a) -> a

addPrefixIsLeq :: f m -> g n -> LeqProof n (m + n)

withAddPrefixLeq :: NatRepr n -> NatRepr m -> (m <= (n + m) => a) -> a

addIsLeqLeft1 :: forall n n' m. LeqProof (n + n') m -> LeqProof n m

dblPosIsPos :: forall n. LeqProof 1 n -> LeqProof 1 (n + n)

leqMulMono :: 1 <= x => p x -> q y -> LeqProof y (x * y)

Arithmetic proof

plusComm :: forall f m g n. f m -> g n -> (m + n) :~: (n + m)

Produce evidence that + is commutative.

mulComm :: forall f m g n. f m -> g n -> (m * n) :~: (n * m)

Produce evidence that * is commutative.

plusMinusCancel :: forall f m g n. f m -> g n -> ((m + n) - n) :~: m

Cancel an add followed b a subtract

minusPlusCancel :: forall f m g n. n <= m => f m -> g n -> ((m - n) + n) :~: m

addMulDistribRight :: forall n m p f g h. f n -> g m -> h p -> ((n * p) + (m * p)) :~: ((n + m) * p)

withAddMulDistribRight :: forall n m p f g h a. f n -> g m -> h p -> (((n * p) + (m * p)) ~ ((n + m) * p) => a) -> a

withSubMulDistribRight :: forall n m p f g h a. m <= n => f n -> g m -> h p -> (((n * p) - (m * p)) ~ ((n - m) * p) => a) -> a

mulCancelR :: (1 <= c, (n1 * c) ~ (n2 * c)) => f1 n1 -> f2 n2 -> f3 c -> n1 :~: n2

mul2Plus :: forall f n. f n -> (n + n) :~: (2 * n)

Re-exports typelists basics

type family (a :: Nat) + (b :: Nat) :: Nat where ... infixl 6

Addition of type-level naturals.

Since: base-4.7.0.0

type family (a :: Nat) - (b :: Nat) :: Nat where ... infixl 6

Subtraction of type-level naturals.

Since: base-4.7.0.0

type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7

Multiplication of type-level naturals.

Since: base-4.7.0.0

type (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ True infix 4

Comparison of type-level naturals, as a constraint.

Since: base-4.7.0.0

class TestEquality (f :: k -> *) where

This class contains types where you can learn the equality of two types from information contained in terms. Typically, only singleton types should inhabit this class.

Minimal complete definition

testEquality

Methods

testEquality :: f a -> f b -> Maybe (a :~: b)

Conditionally prove the equality of a and b.

Instances

TestEquality NatRepr

Defined in Data.Parameterized.NatRepr

Methods

testEquality :: NatRepr a -> NatRepr b -> Maybe (a :~: b)

TestEquality SymbolRepr

Defined in Data.Parameterized.SymbolRepr

Methods

testEquality :: SymbolRepr a -> SymbolRepr b -> Maybe (a :~: b)

TestEquality (Nonce :: k -> *)

Defined in Data.Parameterized.Nonce.Unsafe

Methods

testEquality :: Nonce a -> Nonce b -> Maybe (a :~: b)

TestEquality (TypeRep :: k -> *)

Defined in Data.Typeable.Internal

Methods

testEquality :: TypeRep a -> TypeRep b -> Maybe (a :~: b)

TestEquality (Nonce s :: k -> *)

Defined in Data.Parameterized.Nonce

Methods

testEquality :: Nonce s a -> Nonce s b -> Maybe (a :~: b)

TestEquality ((:~:) a :: k -> *)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

testEquality :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)

TestEquality (Index l :: k -> *)

Defined in Data.Parameterized.List

Methods

testEquality :: Index l a -> Index l b -> Maybe (a :~: b)

TestEquality (Index ctx :: k -> *)

Defined in Data.Parameterized.Context.Unsafe

Methods

testEquality :: Index ctx a -> Index ctx b -> Maybe (a :~: b)

TestEquality (Index ctx :: k -> *)

Defined in Data.Parameterized.Context.Safe

Methods

testEquality :: Index ctx a -> Index ctx b -> Maybe (a :~: b)

TestEquality ((:~~:) a :: k -> *)

Since: base-4.10.0.0

Defined in Data.Type.Equality

Methods

testEquality :: (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b)

TestEquality f => TestEquality (List f :: [k] -> *)

Defined in Data.Parameterized.List

Methods

testEquality :: List f a -> List f b -> Maybe (a :~: b)

TestEquality f => TestEquality (Assignment f :: Ctx k -> *)

Defined in Data.Parameterized.Context.Unsafe

Methods

testEquality :: Assignment f a -> Assignment f b -> Maybe (a :~: b)

TestEquality f => TestEquality (Assignment f :: Ctx k -> *)

Defined in Data.Parameterized.Context.Safe

Methods

testEquality :: Assignment f a -> Assignment f b -> Maybe (a :~: b)

data (a :: k) :~: (b :: k) :: forall k. k -> k -> * where infix 4

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: base-4.7.0.0

Constructors

Refl :: a :~: a

Instances

Category ((:~:) :: k -> k -> *)

Since: base-4.7.0.0

Defined in Control.Category

Methods

id :: a :~: a

(.) :: (b :~: c) -> (a :~: b) -> a :~: c

TestEquality ((:~:) a :: k -> *)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

testEquality :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)

NFData2 ((:~:) :: * -> * -> *)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> ()

NFData1 ((:~:) a)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

liftRnf :: (a0 -> ()) -> (a :~: a0) -> ()

a ~ b => Bounded (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

minBound :: a :~: b

maxBound :: a :~: b

a ~ b => Enum (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b

pred :: (a :~: b) -> a :~: b

toEnum :: Int -> a :~: b

fromEnum :: (a :~: b) -> Int

enumFrom :: (a :~: b) -> [a :~: b]

enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b]

Eq (a :~: b)

Defined in Data.Type.Equality

Methods

(==) :: (a :~: b) -> (a :~: b) -> Bool

(/=) :: (a :~: b) -> (a :~: b) -> Bool

Ord (a :~: b)

Defined in Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering

(<) :: (a :~: b) -> (a :~: b) -> Bool

(<=) :: (a :~: b) -> (a :~: b) -> Bool

(>) :: (a :~: b) -> (a :~: b) -> Bool

(>=) :: (a :~: b) -> (a :~: b) -> Bool

max :: (a :~: b) -> (a :~: b) -> a :~: b

min :: (a :~: b) -> (a :~: b) -> a :~: b

a ~ b => Read (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

readsPrec :: Int -> ReadS (a :~: b)

readList :: ReadS [a :~: b]

readPrec :: ReadPrec (a :~: b)

readListPrec :: ReadPrec [a :~: b]

Show (a :~: b)

Defined in Data.Type.Equality

Methods

showsPrec :: Int -> (a :~: b) -> ShowS

show :: (a :~: b) -> String

showList :: [a :~: b] -> ShowS

NFData (a :~: b)

Since: deepseq-1.4.3.0

Defined in Control.DeepSeq

Methods

rnf :: (a :~: b) -> ()

data Some (f :: k -> *)

Instances

TestEquality f => Eq (Some f)

Defined in Data.Parameterized.Some

Methods

(==) :: Some f -> Some f -> Bool

(/=) :: Some f -> Some f -> Bool

OrdF f => Ord (Some f)

Defined in Data.Parameterized.Some

Methods

compare :: Some f -> Some f -> Ordering

(<) :: Some f -> Some f -> Bool

(<=) :: Some f -> Some f -> Bool

(>) :: Some f -> Some f -> Bool

(>=) :: Some f -> Some f -> Bool

max :: Some f -> Some f -> Some f

min :: Some f -> Some f -> Some f

ShowF f => Show (Some f)

Defined in Data.Parameterized.Some

Methods

showsPrec :: Int -> Some f -> ShowS

show :: Some f -> String

showList :: [Some f] -> ShowS

HashableF f => Hashable (Some f)

Defined in Data.Parameterized.Some

Methods

hashWithSalt :: Int -> Some f -> Int

hash :: Some f -> Int