ixmonad-0.50: Embeds effect systems into Haskell using an parameteric effect monad (the |Effect| type class)

Safe HaskellNone
LanguageHaskell98

Control.Effect.ReaderNat

Documentation

data Nil Source

Instances

Split Nil Nil Nil 
Split Nil (Cons x xs) (Cons x xs) 
Split (Cons x xs) Nil (Cons x xs) 
Split (Cons x Nil) (Cons x Nil) (Cons x Nil) 

data Cons x xs Source

Instances

Split Nil (Cons x xs) (Cons x xs) 
Split (Cons x xs) Nil (Cons x xs) 
Split xs ys zs => Split (Cons (r, x) xs) (Cons (s, y) ys) (Cons (s, y) (Cons (r, x) zs)) 
Split xs ys zs => Split (Cons (r, x) xs) (Cons (s, y) ys) (Cons (r, x) (Cons (s, y) zs)) 
Split xs ys zs => Split (Cons x xs) (Cons x ys) (Cons x zs) 
Split (Cons x Nil) (Cons x Nil) (Cons x Nil) 

data List n where Source

Constructors

Nil :: List Nil 
Cons :: x -> List xs -> List (Cons x xs) 

type family Union s t Source

Equations

Union s t = RemDup (Bubble (Append' s t)) 

type family Append' s t Source

Equations

Append' Nil t = t 
Append' (Cons x xs) ys = Cons x (Append' xs ys) 

data Z Source

Instances

type MinKey (Nat (S m)) (Nat Z) p q = q 
type MinKey (Nat Z) (Nat (S m)) p q = p 
type MinKey (Nat Z) (Nat Z) p q = p 

data S n Source

Instances

type MinKey (Nat (S m)) (Nat (S n)) p q = MinKey (Nat m) (Nat n) p q 
type MinKey (Nat (S m)) (Nat Z) p q = q 
type MinKey (Nat Z) (Nat (S m)) p q = p 

data Nat n where Source

Constructors

Z :: Nat Z 
S :: Nat n -> Nat (S n) 

Instances

type MinKey (Nat (S m)) (Nat (S n)) p q = MinKey (Nat m) (Nat n) p q 
type MinKey (Nat (S m)) (Nat Z) p q = q 
type MinKey (Nat Z) (Nat (S m)) p q = p 
type MinKey (Nat Z) (Nat Z) p q = p 

type family RemDup t Source

Equations

RemDup Nil = Nil 
RemDup (Cons a Nil) = Cons a Nil 
RemDup (Cons a (Cons a as)) = Cons a (RemDup as) 
RemDup (Cons a (Cons b as)) = Cons a (Cons b (RemDup as)) 

type family Bubble l Source

Equations

Bubble Nil = Nil 
Bubble (Cons a Nil) = Cons a Nil 
Bubble (Cons a (Cons b c)) = Cons (Min a b) (Bubble (Cons (Max a b) c)) 

type family Min n m Source

Equations

Min (n, t) (m, t') = MinKey n m (n, t) (m, t') 

type family Max n m Source

Equations

Max (n, t) (m, t') = MinKey m n (n, t) (m, t') 

type family MinKey n m p q Source

Instances

type MinKey (Nat (S m)) (Nat (S n)) p q = MinKey (Nat m) (Nat n) p q 
type MinKey (Nat (S m)) (Nat Z) p q = q 
type MinKey (Nat Z) (Nat (S m)) p q = p 
type MinKey (Nat Z) (Nat Z) p q = p 

data IxReader s a Source

Constructors

IxR 

Fields

unIxR :: List s -> a
 

Instances

Effect * IxReader 
type Unit * IxReader = Nil 
type Plus * IxReader s t = Union s t 
type Inv * IxReader s t = Split s t (Union s t) 

ask :: Nat t -> IxReader (Cons (Nat t, a) Nil) a Source

class Split s t z where Source

Methods

split :: List z -> (List s, List t) Source

Instances

Split Nil Nil Nil 
Split Nil (Cons x xs) (Cons x xs) 
Split (Cons x xs) Nil (Cons x xs) 
Split xs ys zs => Split (Cons (r, x) xs) (Cons (s, y) ys) (Cons (s, y) (Cons (r, x) zs)) 
Split xs ys zs => Split (Cons (r, x) xs) (Cons (s, y) ys) (Cons (r, x) (Cons (s, y) zs)) 
Split xs ys zs => Split (Cons x xs) (Cons x ys) (Cons x zs) 
Split (Cons x Nil) (Cons x Nil) (Cons x Nil)