sessions-2008.3.29: Session Types for HaskellSource codeContentsIndex
Control.Concurrent.Session.Number
Description
Type level Integers. These are all base 10.
Synopsis
data E = E
data D0 n = D0 n
data D1 n = D1 n
data D2 n = D2 n
data D3 n = D3 n
data D4 n = D4 n
data D5 n = D5 n
data D6 n = D6 n
data D7 n = D7 n
data D8 n = D8 n
data D9 n = D9 n
class Succ x y | x -> y where
tySucc :: x -> y
class Pred x y | x -> y where
tyPred :: x -> y
class Add m n s | m n -> s where
tyAdd :: m -> n -> s
class SmallerThan x y
class SmallerThanBool x y res | x y -> res where
isSmallerThan :: x -> y -> res
class TyNum n
class TypeNumberToInt ty where
tyNumToInt :: ty -> Int
Documentation
data E Source
Constructors
E
show/hide Instances
Show E
Reverse' E a a
IncrementRightToLeft E (D1 E)
data D0 n Source
Constructors
D0 n
show/hide Instances
TyListLength Nil (D0 E)
Pred m m' => Add m (D0 E) m
Show n => Show (D0 n)
TypeNumberToInt (D0 E)
TyNum n => TyNum (D0 n)
TyNum (D0 E)
Pred y y' => SmallerThan (D0 E) y
StripLeadingZeros a b => StripLeadingZeros (D0 a) b
Pred' (D0 E) y False
Pred n n' => Add (D0 E) n n
Reverse' n (D0 a) r => Reverse' (D0 n) a r
TyListTake (D0 E) Nil Nil
StripLeadingZeros (D0 E) (D0 E)
DecrementRightToLeft (D1 a) (D0 a)
DecrementRightToLeft a b => DecrementRightToLeft (D0 a) (D9 b)
IncrementRightToLeft a b => IncrementRightToLeft (D9 a) (D0 b)
IncrementRightToLeft (D0 a) (D1 a)
Add (D0 E) (D0 E) (D0 E)
TyListTake (D0 E) (Cons val nxt) Nil
TyListDrop (D0 E) (Cons val nxt) (Cons val nxt)
TyListIndex (Cons res nxt) (D0 E) res
data D1 n Source
Constructors
D1 n
show/hide Instances
IncrementRightToLeft E (D1 E)
Show n => Show (D1 n)
TyNum n => TyNum (D1 n)
TyNum (D1 E)
Pred (D1 a) x' => Pred' (D1 a) x' True
Reverse' n (D1 a) r => Reverse' (D1 n) a r
StripLeadingZeros (D1 a) (D1 a)
DecrementRightToLeft (D2 a) (D1 a)
DecrementRightToLeft (D1 a) (D0 a)
IncrementRightToLeft (D1 a) (D2 a)
IncrementRightToLeft (D0 a) (D1 a)
(TyListTake cnt' nxt nxt', Pred (D1 r) cnt') => TyListTake (D1 r) (Cons val nxt) (Cons val nxt')
data D2 n Source
Constructors
D2 n
show/hide Instances
Show n => Show (D2 n)
TyNum n => TyNum (D2 n)
TyNum (D2 E)
Pred (D2 a) x' => Pred' (D2 a) x' True
Reverse' n (D2 a) r => Reverse' (D2 n) a r
StripLeadingZeros (D2 a) (D2 a)
DecrementRightToLeft (D3 a) (D2 a)
DecrementRightToLeft (D2 a) (D1 a)
IncrementRightToLeft (D2 a) (D3 a)
IncrementRightToLeft (D1 a) (D2 a)
(TyListTake cnt' nxt nxt', Pred (D2 r) cnt') => TyListTake (D2 r) (Cons val nxt) (Cons val nxt')
data D3 n Source
Constructors
D3 n
show/hide Instances
Show n => Show (D3 n)
TyNum n => TyNum (D3 n)
TyNum (D3 E)
Pred (D3 a) x' => Pred' (D3 a) x' True
Reverse' n (D3 a) r => Reverse' (D3 n) a r
StripLeadingZeros (D3 a) (D3 a)
DecrementRightToLeft (D4 a) (D3 a)
DecrementRightToLeft (D3 a) (D2 a)
IncrementRightToLeft (D3 a) (D4 a)
IncrementRightToLeft (D2 a) (D3 a)
(TyListTake cnt' nxt nxt', Pred (D3 r) cnt') => TyListTake (D3 r) (Cons val nxt) (Cons val nxt')
data D4 n Source
Constructors
D4 n
show/hide Instances
Show n => Show (D4 n)
TyNum n => TyNum (D4 n)
TyNum (D4 E)
Pred (D4 a) x' => Pred' (D4 a) x' True
Reverse' n (D4 a) r => Reverse' (D4 n) a r
StripLeadingZeros (D4 a) (D4 a)
DecrementRightToLeft (D5 a) (D4 a)
DecrementRightToLeft (D4 a) (D3 a)
IncrementRightToLeft (D4 a) (D5 a)
IncrementRightToLeft (D3 a) (D4 a)
(TyListTake cnt' nxt nxt', Pred (D4 r) cnt') => TyListTake (D4 r) (Cons val nxt) (Cons val nxt')
data D5 n Source
Constructors
D5 n
show/hide Instances
Show n => Show (D5 n)
TyNum n => TyNum (D5 n)
TyNum (D5 E)
Pred (D5 a) x' => Pred' (D5 a) x' True
Reverse' n (D5 a) r => Reverse' (D5 n) a r
StripLeadingZeros (D5 a) (D5 a)
DecrementRightToLeft (D6 a) (D5 a)
DecrementRightToLeft (D5 a) (D4 a)
IncrementRightToLeft (D5 a) (D6 a)
IncrementRightToLeft (D4 a) (D5 a)
(TyListTake cnt' nxt nxt', Pred (D5 r) cnt') => TyListTake (D5 r) (Cons val nxt) (Cons val nxt')
data D6 n Source
Constructors
D6 n
show/hide Instances
Show n => Show (D6 n)
TyNum n => TyNum (D6 n)
TyNum (D6 E)
Pred (D6 a) x' => Pred' (D6 a) x' True
Reverse' n (D6 a) r => Reverse' (D6 n) a r
StripLeadingZeros (D6 a) (D6 a)
DecrementRightToLeft (D7 a) (D6 a)
DecrementRightToLeft (D6 a) (D5 a)
IncrementRightToLeft (D6 a) (D7 a)
IncrementRightToLeft (D5 a) (D6 a)
(TyListTake cnt' nxt nxt', Pred (D6 r) cnt') => TyListTake (D6 r) (Cons val nxt) (Cons val nxt')
data D7 n Source
Constructors
D7 n
show/hide Instances
Show n => Show (D7 n)
TyNum n => TyNum (D7 n)
TyNum (D7 E)
Pred (D7 a) x' => Pred' (D7 a) x' True
Reverse' n (D7 a) r => Reverse' (D7 n) a r
StripLeadingZeros (D7 a) (D7 a)
DecrementRightToLeft (D8 a) (D7 a)
DecrementRightToLeft (D7 a) (D6 a)
IncrementRightToLeft (D7 a) (D8 a)
IncrementRightToLeft (D6 a) (D7 a)
(TyListTake cnt' nxt nxt', Pred (D7 r) cnt') => TyListTake (D7 r) (Cons val nxt) (Cons val nxt')
data D8 n Source
Constructors
D8 n
show/hide Instances
Show n => Show (D8 n)
TyNum n => TyNum (D8 n)
TyNum (D8 E)
Pred (D8 a) x' => Pred' (D8 a) x' True
Reverse' n (D8 a) r => Reverse' (D8 n) a r
StripLeadingZeros (D8 a) (D8 a)
DecrementRightToLeft (D9 a) (D8 a)
DecrementRightToLeft (D8 a) (D7 a)
IncrementRightToLeft (D8 a) (D9 a)
IncrementRightToLeft (D7 a) (D8 a)
(TyListTake cnt' nxt nxt', Pred (D8 r) cnt') => TyListTake (D8 r) (Cons val nxt) (Cons val nxt')
data D9 n Source
Constructors
D9 n
show/hide Instances
Show n => Show (D9 n)
TyNum n => TyNum (D9 n)
TyNum (D9 E)
Pred (D9 a) x' => Pred' (D9 a) x' True
Reverse' n (D9 a) r => Reverse' (D9 n) a r
StripLeadingZeros (D9 a) (D9 a)
DecrementRightToLeft (D9 a) (D8 a)
DecrementRightToLeft a b => DecrementRightToLeft (D0 a) (D9 b)
IncrementRightToLeft a b => IncrementRightToLeft (D9 a) (D0 b)
IncrementRightToLeft (D8 a) (D9 a)
(TyListTake cnt' nxt nxt', Pred (D9 r) cnt') => TyListTake (D9 r) (Cons val nxt) (Cons val nxt')
class Succ x y | x -> y whereSource
Methods
tySucc :: x -> ySource
class Pred x y | x -> y whereSource
Methods
tyPred :: x -> ySource
class Add m n s | m n -> s whereSource
Methods
tyAdd :: m -> n -> sSource
show/hide Instances
Pred m m' => Add m (D0 E) m
Pred n n' => Add (D0 E) n n
Add (D0 E) (D0 E) (D0 E)
class SmallerThan x y Source
show/hide Instances
Pred y y' => SmallerThan (D0 E) y
class SmallerThanBool x y res | x y -> res whereSource
Methods
isSmallerThan :: x -> y -> resSource
class TyNum n Source
show/hide Instances
TyNum n => TyNum (D9 n)
TyNum (D9 E)
TyNum n => TyNum (D8 n)
TyNum (D8 E)
TyNum n => TyNum (D7 n)
TyNum (D7 E)
TyNum n => TyNum (D6 n)
TyNum (D6 E)
TyNum n => TyNum (D5 n)
TyNum (D5 E)
TyNum n => TyNum (D4 n)
TyNum (D4 E)
TyNum n => TyNum (D3 n)
TyNum (D3 E)
TyNum n => TyNum (D2 n)
TyNum (D2 E)
TyNum n => TyNum (D1 n)
TyNum (D1 E)
TyNum n => TyNum (D0 n)
TyNum (D0 E)
class TypeNumberToInt ty whereSource
Convert a type-level number to an Int. Of course, we can only go this way...
Methods
tyNumToInt :: ty -> IntSource
show/hide Instances
Produced by Haddock version 2.3.0