Copyright	(c) Sirui Lu 2021-2023
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	Safe-Inferred
Language	Haskell2010

Grisette.Utils.Parameterized

Contents

Unsafe axiom
Runtime representation of type-level natural numbers
Proof of KnownNat
Proof of (<=) for type-level natural numbers

Description

Synopsis

unsafeAxiom :: forall a b. a :~: b
data NatRepr (n :: Nat)
natValue :: NatRepr n -> Natural
unsafeMkNatRepr :: Natural -> NatRepr n
natRepr :: forall n. KnownNat n => NatRepr 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 -> NatRepr n -> NatRepr (Div m n)
halfNat :: NatRepr (n + n) -> NatRepr n
data KnownProof (n :: Nat) where
- KnownProof :: KnownNat n => KnownProof n
hasRepr :: forall n. NatRepr n -> KnownProof n
withKnownProof :: KnownProof n -> (KnownNat n => r) -> r
unsafeKnownProof :: Natural -> KnownProof n
knownAdd :: forall m n r. KnownProof m -> KnownProof n -> KnownProof (m + n)
data LeqProof (m :: Nat) (n :: Nat) where
- LeqProof :: m <= n => LeqProof m n
withLeqProof :: LeqProof m n -> (m <= n => r) -> r
unsafeLeqProof :: forall m n. LeqProof m n
testLeq :: NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
leqRefl :: f n -> LeqProof n n
leqSucc :: f n -> LeqProof n (n + 1)
leqTrans :: LeqProof a b -> LeqProof b c -> LeqProof a c
leqZero :: LeqProof 0 n
leqAdd2 :: LeqProof xl xh -> LeqProof yl yh -> LeqProof (xl + yl) (xh + yh)
leqAdd :: LeqProof m n -> f o -> LeqProof m (n + o)
leqAddPos :: (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)

Unsafe axiom

unsafeAxiom :: forall a b. a :~: b Source #

Assert a proof of equality between two types. This is unsafe if used improperly, so use this with caution!

Runtime representation of type-level natural numbers

data NatRepr (n :: Nat) Source #

A runtime representation of type-level natural numbers. This can be used for performing dynamic checks on type-level natural numbers.

natValue :: NatRepr n -> Natural Source #

The underlying runtime natural number value of a type-level natural number.

unsafeMkNatRepr :: Natural -> NatRepr n Source #

Construct a runtime representation of a type-level natural number.

Note: This function is unsafe, as it does not check that the runtime representation is consistent with the type-level representation. You should ensure the consistency yourself or the program can crash or generate incorrect results.

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

Construct a runtime representation of a type-level natural number when its runtime value is known.

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

Decrement a NatRepr by 1.

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

Predecessor of a NatRepr

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

Increment a NatRepr by 1.

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

Addition of two NatReprs.

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

Subtraction of two NatReprs.

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

Division of two NatReprs.

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

Half of a NatRepr.

Proof of KnownNat

data KnownProof (n :: Nat) where Source #

'KnownProof n' is a type whose values are only inhabited when n has a known runtime value.

Constructors

KnownProof :: KnownNat n => KnownProof n

hasRepr :: forall n. NatRepr n -> KnownProof n Source #

Construct a KnownProof given the runtime representation.

withKnownProof :: KnownProof n -> (KnownNat n => r) -> r Source #

Introduces the KnownNat constraint when it's proven.

unsafeKnownProof :: Natural -> KnownProof n Source #

Construct a KnownProof given the runtime value.

Note: This function is unsafe, as it does not check that the runtime representation is consistent with the type-level representation. You should ensure the consistency yourself or the program can crash or generate incorrect results.

knownAdd :: forall m n r. KnownProof m -> KnownProof n -> KnownProof (m + n) Source #

Adding two type-level natural numbers with known runtime values gives a type-level natural number with a known runtime value.

Proof of (<=) for type-level natural numbers

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

'LeqProof m n' is a type whose values are only inhabited when m <= n.

Constructors

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

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

Introduces the m <= n constraint when it's proven.

unsafeLeqProof :: forall m n. LeqProof m n Source #

Construct a LeqProof.

Note: This function is unsafe, as it does not check that the left-hand side is less than or equal to the right-hand side. You should ensure the consistency yourself or the program can crash or generate incorrect results.

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

Checks if a NatRepr is less than or equal to another NatRepr.

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

Apply reflexivity to LeqProof.

leqSucc :: f n -> LeqProof n (n + 1) Source #

A natural number is less than or equal to its successor.

leqTrans :: LeqProof a b -> LeqProof b c -> LeqProof a c Source #

Apply transitivity to LeqProof.

leqZero :: LeqProof 0 n Source #

Zero is less than or equal to any natural number.

leqAdd2 :: LeqProof xl xh -> LeqProof yl yh -> LeqProof (xl + yl) (xh + yh) Source #

Add both sides of two inequalities.

leqAdd :: LeqProof m n -> f o -> LeqProof m (n + o) Source #

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

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

Adding two positive natural numbers is positive.