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 Nat NatRepr

Methods

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

HashableF Nat NatRepr

Methods

hashWithSaltF :: Int -> f tp -> Int

hashF :: f tp -> Int

ShowF Nat NatRepr

Methods

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

showF :: f tp -> String

showsF :: f tp -> String -> String

OrdF Nat NatRepr

Methods

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

leqF :: ktp x -> ktp y -> Bool

ltF :: ktp x -> ktp y -> Bool

geqF :: ktp x -> ktp y -> Bool

gtF :: ktp x -> ktp y -> Bool

KnownNat n => KnownRepr Nat NatRepr n

Methods

knownRepr :: n ctx

Eq (NatRepr m)

Methods

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

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

Show (NatRepr n)

Methods

showsPrec :: Int -> NatRepr n -> ShowS

show :: NatRepr n -> String

showList :: [NatRepr n] -> ShowS

Hashable (NatRepr n)

Methods

hashWithSalt :: Int -> NatRepr n -> Int

hash :: NatRepr n -> Int

PolyEq (NatRepr m) (NatRepr n)

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 :: !(NatRepr y) -> NatComparison x (x + (y + 1))

NatEQ :: NatComparison x x

NatGT :: !(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)

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-i (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)-i (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 -> f 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.

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)

Arithmetic proof

plusComm :: 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

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

Re-exports typelists basics

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

Addition of type-level naturals.

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

Subtraction of type-level naturals.

Since: 4.7.0.0

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

Multiplication of type-level naturals.

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

Comparison of type-level naturals, as a constraint.

class TestEquality k (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 ((:~:) k a b)

Conditionally prove the equality of a and b.

Instances

TestEquality Nat NatRepr

Methods

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

TestEquality Symbol SymbolRepr

Methods

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

TestEquality k (Nonce k)

Methods

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

TestEquality k (Nonce k s)

Methods

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

TestEquality k ((:~:) k a)

Since: 4.7.0.0

Methods

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

TestEquality k (Index k l)

Methods

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

TestEquality k (Index k ctx)

Methods

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

TestEquality k (Index k ctx)

Methods

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

TestEquality k ((:~~:) k1 k a)

Since: 4.10.0.0

Methods

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

TestEquality k f => TestEquality [k] (List k f)

Methods

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

TestEquality k f => TestEquality (Ctx k) (Assignment k f)

Methods

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

TestEquality k f => TestEquality (Ctx k) (Assignment k f)

Methods

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

data (k :~: (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: 4.7.0.0

Constructors

Refl :: (:~:) k a a

Instances

Category k ((:~:) k)

Since: 4.7.0.0

Methods

id :: cat a a

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

TestEquality k ((:~:) k a)

Since: 4.7.0.0

Methods

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

NFData2 ((:~:) *)

Since: 1.4.3.0

Methods

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

NFData1 ((:~:) * a)

Since: 1.4.3.0

Methods

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

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

Since: 4.7.0.0

Methods

minBound :: (k :~: a) b

maxBound :: (k :~: a) b

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

Since: 4.7.0.0

Methods

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

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

toEnum :: Int -> (k :~: a) b

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

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

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

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

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

Eq ((:~:) k a b)

Methods

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

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

Ord ((:~:) k a b)

Methods

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

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

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

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

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

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

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

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

Since: 4.7.0.0

Methods

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

readList :: ReadS [(k :~: a) b]

readPrec :: ReadPrec ((k :~: a) b)

readListPrec :: ReadPrec [(k :~: a) b]

Show ((:~:) k a b)

Methods

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

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

showList :: [(k :~: a) b] -> ShowS

NFData ((:~:) k a b)

Since: 1.4.3.0

Methods

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

data Some (f :: k -> *)

Instances

TestEquality k f => Eq (Some k f)

Methods

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

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

OrdF k f => Ord (Some k f)

Methods

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

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

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

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

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

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

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

ShowF k f => Show (Some k f)

Methods

showsPrec :: Int -> Some k f -> ShowS

show :: Some k f -> String

showList :: [Some k f] -> ShowS

HashableF k f => Hashable (Some k f)

Methods

hashWithSalt :: Int -> Some k f -> Int

hash :: Some k f -> Int