Copyright	(c) Galois Inc 2014-2019
Maintainer	Joe Hendrix <jhendrix@galois.com>
Safe Haskell	Trustworthy
Language	Haskell2010

Data.Parameterized.NatRepr

Contents

Strict order
Bitvector utilities
LeqProof
LeqProof combinators
Arithmetic proof
Re-exports typelists basics

Description

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 value n. This can be used to help use type-level variables on code with data dependendent types.

The TestEquality and DecidableEq instances for NatRepr are 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.

Synopsis

data NatRepr (n :: Nat)
natValue :: NatRepr n -> Natural
intValue :: NatRepr n -> Integer
knownNat :: forall n. KnownNat n => NatRepr n
withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r
data IsZeroNat n where
- ZeroNat :: IsZeroNat 0
- NonZeroNat :: IsZeroNat (n + 1)
isZeroNat :: NatRepr n -> IsZeroNat n
isZeroOrGT1 :: NatRepr n -> Either (n :~: 0) (LeqProof 1 n)
data NatComparison m n where
- 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)
predNat :: NatRepr (n + 1) -> NatRepr n
incNat :: NatRepr n -> NatRepr (n + 1)
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 :: Integral a => a -> Maybe (Some NatRepr)
mkNatRepr :: Natural -> Some NatRepr
maxNat :: NatRepr m -> NatRepr n -> Some NatRepr
natRec :: forall p f. NatRepr p -> f 0 -> (forall n. NatRepr n -> f n -> f (n + 1)) -> f p
natRecStrong :: forall p f. NatRepr p -> f 0 -> (forall n. NatRepr n -> (forall m. m <= n => NatRepr m -> f m) -> f (n + 1)) -> f p
natRecBounded :: forall m h f. m <= h => NatRepr m -> NatRepr h -> f 0 -> (forall n. n <= h => NatRepr n -> f n -> f (n + 1)) -> f (m + 1)
natRecStrictlyBounded :: forall m f. NatRepr m -> f 0 -> (forall n. (n + 1) <= m => NatRepr n -> f n -> f (n + 1)) -> f m
natForEach :: forall l h a. NatRepr l -> NatRepr h -> (forall n. (l <= n, n <= h) => NatRepr n -> a) -> [a]
natFromZero :: forall h a. NatRepr h -> (forall n. n <= h => NatRepr n -> a) -> [a]
data NatCases m n where
- 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
lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void
lessThanAsymmetric :: forall m f n. LeqProof (n + 1) m -> LeqProof (m + 1) n -> f n -> Void
widthVal :: NatRepr n -> Int
minUnsigned :: NatRepr w -> Integer
maxUnsigned :: NatRepr w -> Integer
minSigned :: 1 <= w => NatRepr w -> Integer
maxSigned :: 1 <= w => NatRepr w -> Integer
toUnsigned :: NatRepr w -> Integer -> Integer
toSigned :: 1 <= w => NatRepr w -> Integer -> Integer
unsignedClamp :: NatRepr w -> Integer -> Integer
signedClamp :: 1 <= w => NatRepr w -> Integer -> Integer
data LeqProof (m :: Nat) (n :: Nat) where
- LeqProof :: m <= n => LeqProof m n
decideLeq :: NatRepr a -> NatRepr b -> Either (LeqProof a b) (LeqProof a b -> Void)
testLeq :: forall m n. NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
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
leqSucc :: forall f z. f z -> LeqProof z (z + 1)
leqTrans :: LeqProof m n -> LeqProof n p -> LeqProof m p
leqZero :: LeqProof 0 n
leqAdd2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqSub2 :: LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l - y_h) (x_h - y_l)
leqMulCongr :: LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)
leqProof :: m <= n => f m -> g n -> LeqProof m n
withLeqProof :: LeqProof m n -> (m <= n => a) -> a
isPosNat :: NatRepr n -> Maybe (LeqProof 1 n)
leqAdd :: forall f m n p. LeqProof m n -> f p -> LeqProof m (n + p)
leqSub :: forall m n p. LeqProof m n -> LeqProof p m -> LeqProof (m - p) n
leqMulPos :: forall p q x y. (1 <= x, 1 <= y) => p x -> q y -> LeqProof 1 (x * y)
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)
plusComm :: forall f m g n. f m -> g n -> (m + n) :~: (n + m)
plusAssoc :: forall f m g n h o. f m -> g n -> h o -> (m + (n + o)) :~: ((m + n) + o)
mulComm :: forall f m g n. f m -> g n -> (m * n) :~: (n * m)
plusMinusCancel :: forall f m g n. f m -> g n -> ((m + n) - n) :~: m
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)
lemmaMul :: 1 <= n => p w -> q n -> (w + ((n - 1) * w)) :~: (n * w)
type family (a :: Natural) + (b :: Natural) :: Natural where ...
type family (a :: Natural) - (b :: Natural) :: Natural where ...
type family (a :: Natural) * (b :: Natural) :: Natural where ...
type (<=) (x :: k) (y :: k) = (x <=? y) ~ 'True
class TestEquality (f :: k -> Type) where
- testEquality :: forall (a :: k) (b :: k). f a -> f b -> Maybe (a :~: b)
data (a :: k) :~: (b :: k) where
- Refl :: forall {k} (a :: k). a :~: a
data Some (f :: k -> Type)

Documentation

data NatRepr (n :: Nat) Source #

A runtime presentation of a type-level Nat.

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

Instances

Instances details

TestEquality NatRepr Source #
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods testEquality :: forall (a :: k) (b :: k). NatRepr a -> NatRepr b -> Maybe (a :~: b) #
HashableF NatRepr Source #
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods hashWithSaltF :: forall (tp :: k). Int -> NatRepr tp -> Int Source # hashF :: forall (tp :: k). NatRepr tp -> Int Source #
OrdF NatRepr Source #
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods compareF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> OrderingF x y Source # leqF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool Source # ltF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool Source # geqF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool Source # gtF :: forall (x :: k) (y :: k). NatRepr x -> NatRepr y -> Bool Source #
ShowF NatRepr Source #
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods withShow :: forall p q (tp :: k) a. p NatRepr -> q tp -> (Show (NatRepr tp) => a) -> a Source # showF :: forall (tp :: k). NatRepr tp -> String Source # showsPrecF :: forall (tp :: k). Int -> NatRepr tp -> String -> String Source #
DecidableEq NatRepr Source #
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods decEq :: forall (a :: k) (b :: k). NatRepr a -> NatRepr b -> Either (a :~: b) ((a :~: b) -> Void) Source #
IsRepr NatRepr Source #
Instance details Defined in Data.Parameterized.WithRepr Methods withRepr :: forall (a :: k) r. NatRepr a -> (KnownRepr NatRepr a => r) -> r Source #
KnownNat n => KnownRepr NatRepr (n :: Nat) Source #
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods knownRepr :: NatRepr n Source #
KnownNat n => Data (NatRepr n) Source #
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NatRepr n -> c (NatRepr n) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (NatRepr n) # toConstr :: NatRepr n -> Constr # dataTypeOf :: NatRepr n -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (NatRepr n)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (NatRepr n)) # gmapT :: (forall b. Data b => b -> b) -> NatRepr n -> NatRepr n # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NatRepr n -> r # gmapQ :: (forall d. Data d => d -> u) -> NatRepr n -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NatRepr n -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NatRepr n -> m (NatRepr n) #
Show (NatRepr n) Source #
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods showsPrec :: Int -> NatRepr n -> ShowS # show :: NatRepr n -> String # showList :: [NatRepr n] -> ShowS #
Eq (NatRepr m) Source #
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods (==) :: NatRepr m -> NatRepr m -> Bool # (/=) :: NatRepr m -> NatRepr m -> Bool #
Hashable (NatRepr n) Source #
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods hashWithSalt :: Int -> NatRepr n -> Int # hash :: NatRepr n -> Int #
PolyEq (NatRepr m) (NatRepr n) Source #
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods polyEqF :: NatRepr m -> NatRepr n -> Maybe (NatRepr m :~: NatRepr n) Source # polyEq :: NatRepr m -> NatRepr n -> Bool Source #

natValue :: NatRepr n -> Natural Source #

The underlying natural value of the number.

intValue :: NatRepr n -> Integer Source #

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

This generates a NatRepr from a type-level context.

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

data IsZeroNat n where Source #

Constructors

ZeroNat :: IsZeroNat 0
NonZeroNat :: IsZeroNat (n + 1)

isZeroNat :: NatRepr n -> IsZeroNat n Source #

isZeroOrGT1 :: NatRepr n -> Either (n :~: 0) (LeqProof 1 n) Source #

Every nat is either zero or >= 1.

data NatComparison m n where Source #

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

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

Decrement a NatRepr

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

Get the predecessor of a nat

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

Increment a NatRepr

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

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

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

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

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

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

someNat :: Integral a => a -> Maybe (Some NatRepr) Source #

Turn an Integral value into a NatRepr. Returns Nothing if the given value is negative.

mkNatRepr :: Natural -> Some NatRepr Source #

Turn a Natural into the corresponding NatRepr

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

Return the maximum of two nat representations.

natRec Source #

Arguments

:: forall p f. NatRepr p
-> f 0	base case
-> (forall n. NatRepr n -> f n -> f (n + 1))
-> f p

Recursor for natural numbeers.

natRecStrong Source #

Arguments

:: forall p f. NatRepr p
-> f 0	base case
-> (forall n. NatRepr n -> (forall m. m <= n => NatRepr m -> f m) -> f (n + 1))	inductive step
-> f p

Strong induction variant of the recursor.

natRecBounded :: forall m h f. m <= h => NatRepr m -> NatRepr h -> f 0 -> (forall n. n <= h => NatRepr n -> f n -> f (n + 1)) -> f (m + 1) Source #

Bounded recursor for natural numbers.

If you can prove: - Base case: f 0 - Inductive step: if n <= h and (f n) then (f (n + 1)) You can conclude: for all n <= h, (f (n + 1)).

natRecStrictlyBounded :: forall m f. NatRepr m -> f 0 -> (forall n. (n + 1) <= m => NatRepr n -> f n -> f (n + 1)) -> f m Source #

A version of natRecBounded which doesn't require the type index of the result to be greater than 0 and provides a strict inequality constraint.

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

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

natFromZero :: forall h a. NatRepr h -> (forall n. n <= h => NatRepr n -> a) -> [a] Source #

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

data NatCases m n where Source #

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

Strict order

lessThanIrreflexive :: forall f (a :: Nat). f a -> LeqProof (1 + a) a -> Void Source #

The strict order (<), defined by n < m <-> n + 1 <= m, is irreflexive.

lessThanAsymmetric :: forall m f n. LeqProof (n + 1) m -> LeqProof (m + 1) n -> f n -> Void Source #

The strict order on the naturals is asymmetric

Bitvector utilities

widthVal :: NatRepr n -> Int Source #

Return the value of the nat representation.

minUnsigned :: NatRepr w -> Integer Source #

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

maxUnsigned :: NatRepr w -> Integer Source #

Return maximum unsigned value for bitvector with given width.

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

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

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

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

toUnsigned :: NatRepr w -> Integer -> Integer Source #

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

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

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

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

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

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

LeqProof

data LeqProof (m :: Nat) (n :: Nat) where Source #

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

decideLeq :: NatRepr a -> NatRepr b -> Either (LeqProof a b) (LeqProof a b -> Void) Source #

(<=) is a decidable relation on nats.

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

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

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

Apply reflexivity to LeqProof

leqSucc :: forall f z. f z -> LeqProof z (z + 1) Source #

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

Apply transitivity to LeqProof

leqZero :: LeqProof 0 n Source #

Zero is less than or equal to any Nat.

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

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

Subtract sides of two inequalities.

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

Congruence rule for multiplication

LeqProof combinators

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

Create a leqProof using two proxies

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

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

Test whether natural number is positive.

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

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

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

Multiplying two positive numbers results in a positive number.

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

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

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

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

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

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

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

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

Arithmetic proof

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

Produce evidence that + is commutative.

plusAssoc :: forall f m g n h o. f m -> g n -> h o -> (m + (n + o)) :~: ((m + n) + o) Source #

Produce evidence that + is associative.

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

Produce evidence that * is commutative.

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

Cancel an add followed by a subtract

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

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

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

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

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

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

lemmaMul :: 1 <= n => p w -> q n -> (w + ((n - 1) * w)) :~: (n * w) Source #

Used in Vector

Re-exports typelists basics

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

Addition of type-level naturals.

Since: base-4.7.0.0

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

Subtraction of type-level naturals.

Since: base-4.7.0.0

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

Multiplication of type-level naturals.

Since: base-4.7.0.0

type (<=) (x :: k) (y :: k) = (x <=? y) ~ 'True infix 4 #

Comparison (<=) of comparable types, as a constraint.

Since: base-4.16.0.0

class TestEquality (f :: k -> Type) 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.

Methods

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

Conditionally prove the equality of a and b.

Instances

Instances details

TestEquality NatRepr Source #
Instance details Defined in Data.Parameterized.NatRepr.Internal Methods testEquality :: forall (a :: k) (b :: k). NatRepr a -> NatRepr b -> Maybe (a :~: b) #
TestEquality PeanoRepr Source #
Instance details Defined in Data.Parameterized.Peano Methods testEquality :: forall (a :: k) (b :: k). PeanoRepr a -> PeanoRepr b -> Maybe (a :~: b) #
TestEquality BoolRepr Source #
Instance details Defined in Data.Parameterized.BoolRepr Methods testEquality :: forall (a :: k) (b :: k). BoolRepr a -> BoolRepr b -> Maybe (a :~: b) #
TestEquality SymbolRepr Source #
Instance details Defined in Data.Parameterized.SymbolRepr Methods testEquality :: forall (a :: k) (b :: k). SymbolRepr a -> SymbolRepr b -> Maybe (a :~: b) #
TestEquality (TypeRep :: k -> Type)
Instance details Defined in Data.Typeable.Internal Methods testEquality :: forall (a :: k0) (b :: k0). TypeRep a -> TypeRep b -> Maybe (a :~: b) #
TestEquality (Nonce :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Nonce.Unsafe Methods testEquality :: forall (a :: k0) (b :: k0). Nonce a -> Nonce b -> Maybe (a :~: b) #
TestEquality ((:~:) a :: k -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #
TestEquality (Index ctx :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: forall (a :: k0) (b :: k0). Index ctx a -> Index ctx b -> Maybe (a :~: b) #
TestEquality (Index l :: k -> Type) Source #
Instance details Defined in Data.Parameterized.List Methods testEquality :: forall (a :: k0) (b :: k0). Index l a -> Index l b -> Maybe (a :~: b) #
TestEquality (Nonce s :: k -> Type) Source #
Instance details Defined in Data.Parameterized.Nonce Methods testEquality :: forall (a :: k0) (b :: k0). Nonce s a -> Nonce s b -> Maybe (a :~: b) #
TestEquality ((:~~:) a :: k -> Type)	Since: base-4.10.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) #
TestEquality f => TestEquality (Compose f g :: k2 -> Type)	The deduction (via generativity) that if `g x :~: g y` then `x :~: y`. Since: base-4.14.0.0
Instance details Defined in Data.Functor.Compose Methods testEquality :: forall (a :: k) (b :: k). Compose f g a -> Compose f g b -> Maybe (a :~: b) #
TestEquality f => TestEquality (Assignment f :: Ctx k -> Type) Source #
Instance details Defined in Data.Parameterized.Context.Unsafe Methods testEquality :: forall (a :: k0) (b :: k0). Assignment f a -> Assignment f b -> Maybe (a :~: b) #
TestEquality f => TestEquality (List f :: [k] -> Type) Source #
Instance details Defined in Data.Parameterized.List Methods testEquality :: forall (a :: k0) (b :: k0). List f a -> List f b -> Maybe (a :~: b) #
(TestEquality f, TestEquality g) => TestEquality (PairRepr f g :: (k1, k2) -> Type) Source #
Instance details Defined in Data.Parameterized.DataKind Methods testEquality :: forall (a :: k) (b :: k). PairRepr f g a -> PairRepr f g b -> Maybe (a :~: b) #

data (a :: k) :~: (b :: 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 :: forall {k} (a :: k). a :~: a

Instances

Instances details

Category ((:~:) :: k -> k -> Type)	Since: base-4.7.0.0
Instance details Defined in Control.Category Methods id :: forall (a :: k0). a :~: a # (.) :: forall (b :: k0) (c :: k0) (a :: k0). (b :~: c) -> (a :~: b) -> a :~: c #
TestEquality ((:~:) a :: k -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #
NFData2 ((:~:) :: Type -> Type -> Type)	Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> () #
NFData1 ((:~:) a)	Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf :: (a0 -> ()) -> (a :~: a0) -> () #
(a ~ b, Data a) => Data (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Data Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) # gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b) # toConstr :: (a :~: b) -> Constr # dataTypeOf :: (a :~: b) -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b)) # gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r # gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b) #
a ~ b => Bounded (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods minBound :: a :~: b # maxBound :: a :~: b #
a ~ b => Enum (a :~: b)	Since: base-4.7.0.0
Instance details 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] #
a ~ b => Read (a :~: b)	Since: base-4.7.0.0
Instance details 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)	Since: base-4.7.0.0
Instance details 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
Instance details Defined in Control.DeepSeq Methods rnf :: (a :~: b) -> () #
Eq (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool # (/=) :: (a :~: b) -> (a :~: b) -> Bool #
Ord (a :~: b)	Since: base-4.7.0.0
Instance details 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 #
HasDict (a ~ b) (a :~: b)
Instance details Defined in Data.Constraint Methods evidence :: (a :~: b) -> Dict (a ~ b) #

data Some (f :: k -> Type) Source #

Instances

Instances details

OrdC (Some :: (k -> Type) -> Type) Source #
Instance details Defined in Data.Parameterized.ClassesC Methods compareC :: (forall (x :: k0) (y :: k0). f x -> g y -> OrderingF x y) -> Some f -> Some g -> Ordering Source #
TestEqualityC (Some :: (k -> Type) -> Type) Source #	This instance demonstrates where the above class is useful: namely, in types with existential quantification.
Instance details Defined in Data.Parameterized.ClassesC Methods testEqualityC :: (forall (x :: k0) (y :: k0). f x -> f y -> Maybe (x :~: y)) -> Some f -> Some f -> Bool Source #
FoldableF (Some :: (k -> Type) -> Type) Source #
Instance details Defined in Data.Parameterized.Some Methods foldMapF :: Monoid m => (forall (s :: k0). e s -> m) -> Some e -> m Source # foldrF :: (forall (s :: k0). e s -> b -> b) -> b -> Some e -> b Source # foldlF :: (forall (s :: k0). b -> e s -> b) -> b -> Some e -> b Source # foldrF' :: (forall (s :: k0). e s -> b -> b) -> b -> Some e -> b Source # foldlF' :: (forall (s :: k0). b -> e s -> b) -> b -> Some e -> b Source # toListF :: (forall (tp :: k0). f tp -> a) -> Some f -> [a] Source #
FunctorF (Some :: (k -> Type) -> Type) Source #
Instance details Defined in Data.Parameterized.Some Methods fmapF :: (forall (x :: k0). f x -> g x) -> Some f -> Some g Source #
TraversableF (Some :: (k -> Type) -> Type) Source #
Instance details Defined in Data.Parameterized.Some Methods traverseF :: Applicative m => (forall (s :: k0). e s -> m (f s)) -> Some e -> m (Some f) Source #
ShowF f => Show (Some f) Source #
Instance details Defined in Data.Parameterized.Some Methods showsPrec :: Int -> Some f -> ShowS # show :: Some f -> String # showList :: [Some f] -> ShowS #
TestEquality f => Eq (Some f) Source #
Instance details Defined in Data.Parameterized.Some Methods (==) :: Some f -> Some f -> Bool # (/=) :: Some f -> Some f -> Bool #
OrdF f => Ord (Some f) Source #
Instance details 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 #
(HashableF f, TestEquality f) => Hashable (Some f) Source #
Instance details Defined in Data.Parameterized.Some Methods hashWithSalt :: Int -> Some f -> Int # hash :: Some f -> Int #