DDF.DBI

Documentation

class Monoid r m where

Minimal complete definition

zero, plus

Methods

zero :: r h m

plus :: r h (m -> m -> m)

class DBI r where

Minimal complete definition

z, s, abs, app, liftEnv

Methods

z :: r (a, h) a

s :: r h b -> r (a, h) b

abs :: r (a, h) b -> r h (a -> b)

app :: r h (a -> b) -> r h a -> r h b

hoas :: (r (a, h) a -> r (a, h) b) -> r h (a -> b)

We use a variant of HOAS so it can be compile to DBI, which is more compositional (No Negative Occurence). It require explicit lifting of variables. Use lam to do automatic lifting of variables.

liftEnv :: r () x -> r h x

com :: r h ((b -> c) -> (a -> b) -> a -> c)

flip :: r h ((a -> b -> c) -> b -> a -> c)

id :: r h (a -> a)

const :: r h (a -> b -> a)

scomb :: r h ((a -> b -> c) -> (a -> b) -> a -> c)

dup :: r h ((a -> a -> b) -> a -> b)

let_ :: r h (a -> (a -> b) -> b)

Instances

DBI Show

Methods

z :: Show (a, h) a

s :: Show h b -> Show (a, h) b

abs :: Show (a, h) b -> Show h (a -> b)

app :: Show h (a -> b) -> Show h a -> Show h b

hoas :: (Show (a, h) a -> Show (a, h) b) -> Show h (a -> b)

liftEnv :: Show () x -> Show h x

com :: Show h ((b -> c) -> (a -> b) -> a -> c)

flip :: Show h ((a -> b -> c) -> b -> a -> c)

id :: Show h (a -> a)

const :: Show h (a -> b -> a)

scomb :: Show h ((a -> b -> c) -> (a -> b) -> a -> c)

dup :: Show h ((a -> a -> b) -> a -> b)

let_ :: Show h (a -> (a -> b) -> b)

DBI Size

Methods

z :: Size (a, h) a

s :: Size h b -> Size (a, h) b

abs :: Size (a, h) b -> Size h (a -> b)

app :: Size h (a -> b) -> Size h a -> Size h b

hoas :: (Size (a, h) a -> Size (a, h) b) -> Size h (a -> b)

liftEnv :: Size () x -> Size h x

com :: Size h ((b -> c) -> (a -> b) -> a -> c)

flip :: Size h ((a -> b -> c) -> b -> a -> c)

id :: Size h (a -> a)

const :: Size h (a -> b -> a)

scomb :: Size h ((a -> b -> c) -> (a -> b) -> a -> c)

dup :: Size h ((a -> a -> b) -> a -> b)

let_ :: Size h (a -> (a -> b) -> b)

DBI UInt

Methods

z :: UInt (a, h) a

s :: UInt h b -> UInt (a, h) b

abs :: UInt (a, h) b -> UInt h (a -> b)

app :: UInt h (a -> b) -> UInt h a -> UInt h b

hoas :: (UInt (a, h) a -> UInt (a, h) b) -> UInt h (a -> b)

liftEnv :: UInt () x -> UInt h x

com :: UInt h ((b -> c) -> (a -> b) -> a -> c)

flip :: UInt h ((a -> b -> c) -> b -> a -> c)

id :: UInt h (a -> a)

const :: UInt h (a -> b -> a)

scomb :: UInt h ((a -> b -> c) -> (a -> b) -> a -> c)

dup :: UInt h ((a -> a -> b) -> a -> b)

let_ :: UInt h (a -> (a -> b) -> b)

(Prod r, Unit r) => DBI (UnLiftEnv r)

Methods

z :: UnLiftEnv r (a, h) a

s :: UnLiftEnv r h b -> UnLiftEnv r (a, h) b

abs :: UnLiftEnv r (a, h) b -> UnLiftEnv r h (a -> b)

app :: UnLiftEnv r h (a -> b) -> UnLiftEnv r h a -> UnLiftEnv r h b

hoas :: (UnLiftEnv r (a, h) a -> UnLiftEnv r (a, h) b) -> UnLiftEnv r h (a -> b)

liftEnv :: UnLiftEnv r () x -> UnLiftEnv r h x

com :: UnLiftEnv r h ((b -> c) -> (a -> b) -> a -> c)

flip :: UnLiftEnv r h ((a -> b -> c) -> b -> a -> c)

id :: UnLiftEnv r h (a -> a)

const :: UnLiftEnv r h (a -> b -> a)

scomb :: UnLiftEnv r h ((a -> b -> c) -> (a -> b) -> a -> c)

dup :: UnLiftEnv r h ((a -> a -> b) -> a -> b)

let_ :: UnLiftEnv r h (a -> (a -> b) -> b)

const1 :: DBI r => r h a -> r h (b -> a)

map2 :: (Functor * r f, DBI r) => r h (a -> b) -> r h (f a) -> r h (f b)

return :: Applicative k r a => r h (x -> a x)

bind2 :: Monad r m => r h (m a) -> r h (a -> m b) -> r h (m b)

map1 :: (Functor * r f, DBI r) => r h (a -> b) -> r h (f a -> f b)

join1 :: Monad r m => r h (m (m a)) -> r h (m a)

bimap2 :: (BiFunctor * r p, DBI r) => r h (a -> b) -> r h (c -> d) -> r h (p a c -> p b d)

bimap3 :: (BiFunctor * r p, DBI r) => r h (a -> b) -> r h (c -> d) -> r h (p a c) -> r h (p b d)

flip1 :: DBI r => r h (a -> b -> c) -> r h (b -> a -> c)

flip2 :: DBI r => r h (a1 -> a -> c) -> r h a -> r h (a1 -> c)

let_2 :: DBI r => r h a -> r h (a -> b) -> r h b

class Functor r f where

Minimal complete definition

map

Methods

map :: r h ((a -> b) -> f a -> f b)

class Functor r a => Applicative r a where

Minimal complete definition

pure, ap

Methods

pure :: r h (x -> a x)

ap :: r h (a (x -> y) -> a x -> a y)

class (DBI r, Applicative r m) => Monad r m where

Minimal complete definition

join | bind

Methods

bind :: r h (m a -> (a -> m b) -> m b)

join :: r h (m (m a) -> m a)

class BiFunctor r p where

Minimal complete definition

bimap

Methods

bimap :: r h ((a -> b) -> (c -> d) -> p a c -> p b d)

app3 :: DBI r => r h (a2 -> a1 -> a -> b) -> r h a2 -> r h a1 -> r h a -> r h b

com2 :: DBI r => r h (b -> c) -> r h (a -> b) -> r h (a -> c)

class NT repr l r where

Minimal complete definition

conv

Methods

conv :: repr l t -> repr r t

Instances

NT k k1 repr x x

Methods

conv :: x l t -> x r t

NTS k k1 repr l r => NT k k1 repr l r

Methods

conv :: r l t -> r r t

class NTS repr l r where

Minimal complete definition

convS

Methods

convS :: repr l t -> repr r t

Instances

(DBI repr, NT * * repr l r) => NTS * * repr l (a, r)

Methods

convS :: (a, r) l t -> (a, r) r t

lam :: forall repr a b h. DBI repr => ((forall k. NT repr (a, h) k => repr k a) -> repr (a, h) b) -> repr h (a -> b)

lam2 :: forall repr a b c h. DBI repr => ((forall k. NT repr (a, h) k => repr k a) -> (forall k. NT repr (b, (a, h)) k => repr k b) -> repr (b, (a, h)) c) -> repr h (a -> b -> c)

lam3 :: (NT * * repr (a, (b1, (a1, h))) k, NT * * repr (b1, (a1, h)) k1, NT * * repr (a1, h) k2, DBI repr) => (repr k2 a1 -> repr k1 b1 -> repr k a -> repr (a, (b1, (a1, h))) b) -> repr h (a1 -> b1 -> a -> b)

app2 :: DBI r => r h (a1 -> a -> b) -> r h a1 -> r h a -> r h b

plus2 :: (Monoid * r b, DBI r) => r h b -> r h b -> r h b

noEnv :: repr () x -> repr () x

scomb2 :: DBI r => r h (a -> b -> c) -> r h (a -> b) -> r h (a -> c)

module DDF.ImportMeta