effect-monad-0.8.1.0: Embeds effect systems and program logics into Haskell using graded monads and parameterised monads

Safe HaskellNone
LanguageHaskell98

Control.Effect.Vector

Documentation

data Z Source #

Instances

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

data S n Source #

Instances

type Add (S n) m Source # 
type Add (S n) m = S (Add n m)
type Plus * Vector (S n) m Source # 
type Plus * Vector (S n) m = Add m (Plus * Vector 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 Source # 

Associated Types

type Unit Vector (m :: Vector -> * -> *) :: k Source #

type Plus Vector (m :: Vector -> * -> *) (f :: Vector) (g :: Vector) :: k Source #

type Inv Vector (m :: Vector -> * -> *) (f :: Vector) (g :: Vector) :: Constraint Source #

Methods

return :: a -> m (Unit Vector m) a Source #

(>>=) :: Inv Vector m f g => m f a -> (a -> m g b) -> m (Plus Vector m f g) b Source #

(>>) :: Inv Vector m f g => m f a -> m g b -> m (Plus Vector m f g) b Source #

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

type family Add s t Source #

Instances

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

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