sessions-2008.7.18: Session Types for Haskell Source code Contents Index

Control.Concurrent.Session.Base.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 Instances Show E Reverse' E a a IncrementRightToLeft E (D1 E)

data D0 n Source

Constructors D0 n 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 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 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 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 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 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 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 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 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 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 where Source

Methods tySucc :: x -> y Source

class Pred x y | x -> y where Source

Methods tyPred :: x -> y Source

class Add m n s | m n -> s where Source

Methods tyAdd :: m -> n -> s Source 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

Instances Pred y y' => SmallerThan (D0 E) y

class SmallerThanBool x y res | x y -> res where Source

Methods isSmallerThan :: x -> y -> res Source

class TyNum n Source

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

Convert a type-level number to an Int. Of course, we can only go this way... Methods tyNumToInt :: ty -> Int Source Instances TypeNumberToInt (D0 E)

Produced by Haddock version 2.4.2