sessions-2008.2.23: Session Types for Haskell

Control.Concurrent.Session.Number

Description

Type level Integers. These are all base 10.

Synopsis

Documentation

data E Source

Constructors

E 

Instances

Show E 
Reverse' E a a 
IncrementRightToLeft E (D1 E) 
ListLength Nil (D0 E) 
Pred m m' => Add m (D0 E) m 
TypeNumberToInt (D0 E) 
TyNum (D9 E) 
TyNum (D8 E) 
TyNum (D7 E) 
TyNum (D6 E) 
TyNum (D5 E) 
TyNum (D4 E) 
TyNum (D3 E) 
TyNum (D2 E) 
TyNum (D1 E) 
TyNum (D0 E) 
Pred y y' => SmallerThan (D0 E) y 
Pred n n' => Add (D0 E) n n 
StripLeadingZeros (D0 E) (D0 E) 
Add (D0 E) (D0 E) (D0 E) 
Elem (Cons res nxt) (D0 E) res 

data D0 n Source

Constructors

D0 n 

Instances

ListLength 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 n n' => Add (D0 E) n n 
Reverse' n (D0 a) r => Reverse' (D0 n) a r 
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) 
Elem (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) 
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) 

data D2 n Source

Constructors

D2 n 

Instances

Show n => Show (D2 n) 
TyNum n => TyNum (D2 n) 
TyNum (D2 E) 
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) 

data D3 n Source

Constructors

D3 n 

Instances

Show n => Show (D3 n) 
TyNum n => TyNum (D3 n) 
TyNum (D3 E) 
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) 

data D4 n Source

Constructors

D4 n 

Instances

Show n => Show (D4 n) 
TyNum n => TyNum (D4 n) 
TyNum (D4 E) 
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) 

data D5 n Source

Constructors

D5 n 

Instances

Show n => Show (D5 n) 
TyNum n => TyNum (D5 n) 
TyNum (D5 E) 
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) 

data D6 n Source

Constructors

D6 n 

Instances

Show n => Show (D6 n) 
TyNum n => TyNum (D6 n) 
TyNum (D6 E) 
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) 

data D7 n Source

Constructors

D7 n 

Instances

Show n => Show (D7 n) 
TyNum n => TyNum (D7 n) 
TyNum (D7 E) 
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) 

data D8 n Source

Constructors

D8 n 

Instances

Show n => Show (D8 n) 
TyNum n => TyNum (D8 n) 
TyNum (D8 E) 
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) 

data D9 n Source

Constructors

D9 n 

Instances

Show n => Show (D9 n) 
TyNum n => TyNum (D9 n) 
TyNum (D9 E) 
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) 

class Succ x y | x -> y whereSource

Methods

tySucc :: x -> ySource

Instances

(Reverse a a', IncrementRightToLeft a' b', Reverse b' b) => Succ a b 

class Pred x y | x -> y whereSource

Methods

tyPred :: x -> ySource

Instances

(Reverse a a', DecrementRightToLeft a' b', Reverse b' b'', StripLeadingZeros b'' b) => Pred a b 

class Add m n s | m n -> s whereSource

Methods

tyAdd :: m -> n -> sSource

Instances

(Add m' n' s, Pred m m', Pred n n', Succ s s', Succ s' s'') => Add m n s'' 
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 x x', Pred y y', SmallerThan x' y') => SmallerThan x y 
Pred y y' => SmallerThan (D0 E) y 

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 whereSource

Convert a type-level number to an Int. Of course, we can only go this way...

Methods

tyNumToInt :: ty -> IntSource

Instances