effect-monad-0.6.1: Embeds effect systems into Haskell using parameteric effect monads

Safe HaskellNone
LanguageHaskell98

Control.Effect.Vector

Documentation

data Z Source

Instances

type Add Z m = m 
type Plus * Vector Z m = Z 

data S n Source

Instances

type Plus * Vector (S n) m = Add m (Plus * Vector n m) 
type Add (S n) m = S (Add n m) 

data Vector n a where Source

Constructors

Nil :: Vector Z a 
Cons :: a -> Vector n a -> Vector (S n) a 

Instances

Effect * Vector 
type Unit * Vector = S Z 
type Plus * Vector Z m = Z 
type Inv * Vector s t = () 
type Plus * Vector (S n) m = Add m (Plus * Vector n m) 

type family Add s t Source

Instances

type Add Z m = m 
type Add (S n) m = S (Add n m) 

append :: Vector n a -> Vector m a -> Vector (Add n m) a Source