| Copyright | (c) Erich Gut |
|---|---|
| License | BSD3 |
| Maintainer | zerich.gut@gmail.com |
| Safe Haskell | None |
| Language | Haskell2010 |
OAlg.Entity.Natural
Description
natural numbers promotable to type-level. They serve to parameterize the length of finite lists on type-level (see OAlg.Entity.FinList).
Note We need the language extension UndecidableInstances for type checking the definition
N0 * m = N0 S n * m = m + n * m
for the type family *.
Using UndecidableInstances could cause the type checker to not terminate, but this will
obviously not happen for the given definition (we also use the same definition for the
multiplicative structure of N').
Synopsis
- data N'
- toN' :: N -> N'
- type family (n :: N') + (m :: k) :: N'
- type family (n :: k) * (m :: N') :: N'
- data (n :: N') :<=: (m :: N') where
- nodAnyFst :: forall (i :: N') (n :: N'). (i :<=: n) -> Any i
- nodAnySnd :: forall (i :: N') (n :: N'). (i :<=: n) -> Any n
- nodRefl :: forall (n :: N'). Any n -> n :<=: n
- nodPred :: forall (n :: N') (m :: N'). ((n + 1) :<=: m) -> n :<=: m
- class Typeable n => Attestable (n :: N') where
- data Ats (n :: N') where
- Ats :: forall (n :: N'). Attestable n => Ats n
- ats :: forall (n :: N'). Any n -> Ats n
- atsSucc :: forall (n :: N'). Ats n -> Ats (n + 1)
- nValue :: forall (n :: N') p. Attestable n => p n -> N
- data W (n :: N') where
- cmpW :: forall (n :: N') (m :: N'). W n -> W m -> Ordering
- (++) :: forall (n :: N') (m :: N'). W n -> W m -> W (n + m)
- (**) :: forall (n :: N') (m :: N'). W n -> W m -> W (n * m)
- data W' = W' (W n)
- toW' :: N -> W'
- data SomeNatural where
- SomeNatural :: forall (n :: N'). Attestable n => W n -> SomeNatural
- succSomeNatural :: SomeNatural -> SomeNatural
- someNatural :: N -> SomeNatural
- naturals :: [SomeNatural]
- induction :: forall (n :: N') f. Any n -> f N0 -> (forall (i :: N'). f i -> f (i + 1)) -> f n
- type Any = W
- type Some = W'
- refl :: forall (x :: N'). Any x -> x :~: x
- lemma1 :: forall {k1} {k2} (x :: k1) (y :: k1) (f :: k1 -> k2). (x :~: y) -> f x :~: f y
- sbstAdd :: forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k). (a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b')
- prpAdd0 :: forall (a :: N'). (a + 0) :~: a
- prpAdd1 :: forall (a :: N'). (a + 1) :~: 'S a
- prpAdd2 :: forall (a :: N'). (a + 2) :~: 'S ('S a)
- prpEqlAny :: forall (n :: N') (m :: N'). (Any n :~: Any m) -> n :~: m
- prpEqlAny' :: forall (n :: N') (m :: N'). (n :~: m) -> Any n :~: Any m
- prpSuccInjective :: forall (n :: N') (m :: N'). ('S n :~: 'S m) -> n :~: m
- prpAddNtrlL :: forall p (a :: N'). p a -> (N0 + a) :~: a
- prpAddNtrlR :: forall (a :: N'). Any a -> (a + N0) :~: a
- prpAddAssoc :: forall (a :: N') (b :: N') (c :: N'). Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c))
- lemmaAdd1 :: forall (a :: N') (b :: N'). Any a -> Any b -> ('S a + b) :~: (a + 'S b)
- prpAddComm :: forall (a :: N') (b :: N'). Any a -> Any b -> (a + b) :~: (b + a)
- prpMltNtrlL :: forall (a :: N'). Any a -> (N1 * a) :~: a
- prpMltNtrlR :: forall (a :: N'). Any a -> (a * N1) :~: a
- prpDstrL :: forall (a :: N') (b :: N') (c :: N'). Any a -> Any b -> Any c -> ((a + b) * c) :~: ((a * c) + (b * c))
- prpMltAssoc :: forall (a :: N') (b :: N') (c :: N'). Any a -> Any b -> Any c -> ((a * b) * c) :~: (a * (b * c))
- lemmaMlt1 :: forall (a :: N'). Any a -> (a * N0) :~: N0
- lemmaAdd2 :: forall (a :: N') (b :: N') (c :: N'). Any a -> Any b -> Any c -> (a + (b + c)) :~: (b + (a + c))
- prpDstrR :: forall (a :: N') (b :: N') (c :: N'). Any a -> Any b -> Any c -> (a * (b + c)) :~: ((a * b) + (a * c))
- prpMltComm :: forall (a :: N') (b :: N'). Any a -> Any b -> (a * b) :~: (b * a)
- codeW :: N -> N -> String
- itfW :: N -> N -> String
- type N0 = 'N0
- type N1 = 'S N0
- type N2 = 'S N1
- type N3 = 'S N2
- type N4 = 'S N3
- type N5 = 'S N4
- type N6 = 'S N5
- type N7 = 'S N6
- type N8 = 'S N7
- type N9 = 'S N8
- type N10 = 'S N9
- xSomeNatural :: X N -> X SomeNatural
Natrual Numbers
natural number promotable to type-level.
Instances
type family (n :: N') + (m :: k) :: N' infixr 6 Source #
addition of natural numbers.
Instances
| type N0 + (n :: N') Source # | |
Defined in OAlg.Entity.Natural | |
| type n + 0 Source # | |
Defined in OAlg.Entity.Natural type n + 0 = n | |
| type n + 1 Source # | |
Defined in OAlg.Entity.Natural | |
| type n + 2 Source # | |
Defined in OAlg.Entity.Natural | |
| type n + 3 Source # | |
Defined in OAlg.Entity.Natural | |
| type ('S n) + (m :: N') Source # | |
type family (n :: k) * (m :: N') :: N' infixr 7 Source #
multiplication of natural numbers.
Ordering
nodAnyFst :: forall (i :: N') (n :: N'). (i :<=: n) -> Any i Source #
the induced witness of the first component.
nodAnySnd :: forall (i :: N') (n :: N'). (i :<=: n) -> Any n Source #
the induced witness of the second component.
nodPred :: forall (n :: N') (m :: N'). ((n + 1) :<=: m) -> n :<=: m Source #
if n is smaler or equal to + 1m then n is also smaler of equal
to m.
Attest
class Typeable n => Attestable (n :: N') where Source #
attest for any natural number.
Instances
| Attestable N0 Source # | |
| Attestable n => Attestable ('S n) Source # | |
data Ats (n :: N') where Source #
witness of being attestable.
Constructors
| Ats :: forall (n :: N'). Attestable n => Ats n |
nValue :: forall (n :: N') p. Attestable n => p n -> N Source #
the corresponding natural number in N of a type parameterized by n.
data W (n :: N') where Source #
witness for a natural number and serves for inductively definable elements (see induction).
(**) :: forall (n :: N') (m :: N'). W n -> W m -> W (n * m) infixr 7 Source #
multiplication of witnesses.
Instances
data SomeNatural where Source #
witnesse of some natural.
Constructors
| SomeNatural :: forall (n :: N'). Attestable n => W n -> SomeNatural |
Instances
| Show SomeNatural Source # | |
Defined in OAlg.Entity.Natural Methods showsPrec :: Int -> SomeNatural -> ShowS # show :: SomeNatural -> String # showList :: [SomeNatural] -> ShowS # | |
| Eq SomeNatural Source # | |
Defined in OAlg.Entity.Natural | |
| Validable SomeNatural Source # | |
Defined in OAlg.Entity.Natural Methods valid :: SomeNatural -> Statement Source # | |
succSomeNatural :: SomeNatural -> SomeNatural Source #
successor of some natural number.
someNatural :: N -> SomeNatural Source #
mapping N to SomeNatural.
Note The implementation of this mapping is quite inefficent for high values of N.
naturals :: [SomeNatural] Source #
the infinite list of some naturals.
Induction
induction :: forall (n :: N') f. Any n -> f N0 -> (forall (i :: N'). f i -> f (i + 1)) -> f n Source #
induction for general type functions.
Propositions
The following propositions are based - for the most part - on induction.
To ensure that the proofs yield a terminal value, i.e. Refl, we
used in the proof of the induction hypothesis only propositions which
are proofed before. So: if these propositions terminate, then also
the hypothesis will terminate.
Some basic Lemmas
lemma1 :: forall {k1} {k2} (x :: k1) (y :: k1) (f :: k1 -> k2). (x :~: y) -> f x :~: f y Source #
well definition of parameterized types.
sbstAdd :: forall {k} (a :: N') (a' :: N') (b :: k) (b' :: k). (a :~: a') -> (b :~: b') -> (a + b) :~: (a' + b') Source #
substitution rule for addition.
Some abbreviations
prpAdd2 :: forall (a :: N'). (a + 2) :~: 'S ('S a) Source #
adding 2 is equal to the successor of the successor.
Equivalence of Any
prpEqlAny :: forall (n :: N') (m :: N'). (Any n :~: Any m) -> n :~: m Source #
equality of the underlying natural number.
prpEqlAny' :: forall (n :: N') (m :: N'). (n :~: m) -> Any n :~: Any m Source #
Any is as parameterized type is well defined.
Injectivity of the Successor
prpSuccInjective :: forall (n :: N') (m :: N'). ('S n :~: 'S m) -> n :~: m Source #
successor is injective.
Addition
Neutral Element
N0 is the neutral element of +.
prpAddNtrlL :: forall p (a :: N'). p a -> (N0 + a) :~: a Source #
N0 is left neutral for the addition.
prpAddNtrlR :: forall (a :: N'). Any a -> (a + N0) :~: a Source #
N0 is the right neutral for the addition.
Associativity
prpAddAssoc :: forall (a :: N') (b :: N') (c :: N'). Any a -> Any b -> Any c -> ((a + b) + c) :~: (a + (b + c)) Source #
addition is associative.
Commutativity
lemmaAdd1 :: forall (a :: N') (b :: N'). Any a -> Any b -> ('S a + b) :~: (a + 'S b) Source #
lemma 1 for the addition.
prpAddComm :: forall (a :: N') (b :: N'). Any a -> Any b -> (a + b) :~: (b + a) Source #
addition is commutative.
Multiplication
prpMltNtrlL :: forall (a :: N'). Any a -> (N1 * a) :~: a Source #
N1 is left neutral for the multiplication.
prpMltNtrlR :: forall (a :: N'). Any a -> (a * N1) :~: a Source #
N1 is right neutral for the multiplication.
Distributivity on the left
prpDstrL :: forall (a :: N') (b :: N') (c :: N'). Any a -> Any b -> Any c -> ((a + b) * c) :~: ((a * c) + (b * c)) Source #
law of left distributivity holds.
Associativity
prpMltAssoc :: forall (a :: N') (b :: N') (c :: N'). Any a -> Any b -> Any c -> ((a * b) * c) :~: (a * (b * c)) Source #
multiplication is associative.
Distributivity on the right
lemmaAdd2 :: forall (a :: N') (b :: N') (c :: N'). Any a -> Any b -> Any c -> (a + (b + c)) :~: (b + (a + c)) Source #
lemma 2 for addition.
prpDstrR :: forall (a :: N') (b :: N') (c :: N'). Any a -> Any b -> Any c -> (a * (b + c)) :~: ((a * b) + (a * c)) Source #
law of right distributivity holds.
Commutativity
prpMltComm :: forall (a :: N') (b :: N'). Any a -> Any b -> (a * b) :~: (b * a) Source #
multiplication is commutative.
Some attests
generating the Haskell code and interface for witnesses.
itfW :: N -> N -> String Source #
itfW n m generates the haskell interface for the witnesses W from n to m.
X
xSomeNatural :: X N -> X SomeNatural Source #
the induced random variable for some natural number.