DDF.DBI

Documentation

class Monoid r m where

Minimal complete definition

zero, plus

Methods

zero :: r h m

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

Instances

Lang repr => ProdCon (Monoid * repr) l r

Methods

prodCon :: (Monoid * repr l, Monoid * repr r) :- Monoid * repr (l, r)

class DBI r where

Minimal complete definition

z, s, abs, app

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.

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 Eval

Methods

z :: Eval (a, h) a

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

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

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

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

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

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

id :: Eval h (a -> a)

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

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

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

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

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)

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)

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 r => DBI (P r)

Methods

z :: P r (a, h) a

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

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

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

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

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

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

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

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

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

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

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

SubL c DBI => DBI (Term c)

Methods

z :: Term c (a, h) a

s :: Term c h b -> Term c (a, h) b

abs :: Term c (a, h) b -> Term c h (a -> b)

app :: Term c h (a -> b) -> Term c h a -> Term c h b

hoas :: (Term c (a, h) a -> Term c (a, h) b) -> Term c h (a -> b)

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

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

id :: Term c h (a -> a)

const :: Term c h (a -> b -> a)

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

dup :: Term c h ((a -> a -> b) -> a -> b)

let_ :: Term c h (a -> (a -> b) -> b)

DBI repr => DBI (UnHOAS repr)

Methods

z :: UnHOAS repr (a, h) a

s :: UnHOAS repr h b -> UnHOAS repr (a, h) b

abs :: UnHOAS repr (a, h) b -> UnHOAS repr h (a -> b)

app :: UnHOAS repr h (a -> b) -> UnHOAS repr h a -> UnHOAS repr h b

hoas :: (UnHOAS repr (a, h) a -> UnHOAS repr (a, h) b) -> UnHOAS repr h (a -> b)

com :: UnHOAS repr h ((b -> c) -> (a -> b) -> a -> c)

flip :: UnHOAS repr h ((a -> b -> c) -> b -> a -> c)

id :: UnHOAS repr h (a -> a)

const :: UnHOAS repr h (a -> b -> a)

scomb :: UnHOAS repr h ((a -> b -> c) -> (a -> b) -> a -> c)

dup :: UnHOAS repr h ((a -> a -> b) -> a -> b)

let_ :: UnHOAS repr h (a -> (a -> b) -> b)

Prod 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)

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)

Prod r => DBI (ImpW r)

Methods

z :: ImpW r (a, h) a

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

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

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

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

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

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

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

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

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

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

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

type SubLC c DBI

type SubLC c DBI = ()

class LiftEnv r where

Minimal complete definition

liftEnv

Methods

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

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

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

return :: Applicative 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 => 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 DBI r => Functor r f where

Minimal complete definition

map

Methods

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

Instances

Functor r x => Functor (UnHOAS r) x

Methods

map :: UnHOAS r h ((a -> b) -> x a -> x 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)

Instances

Applicative r x => Applicative (UnHOAS r) x

Methods

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

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

pure1 :: Applicative r a => r h a1 -> r h (a a1)

ap1 :: Applicative r a => r h (a (x -> y)) -> r h (a x -> a y)

ap2 :: Applicative r a => r h (a (x -> y)) -> r h (a x) -> r h (a y)

class 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)

Instances

Monad r x => Monad (UnHOAS r) x

Methods

bind :: UnHOAS r h (x a -> (a -> x b) -> x b)

join :: UnHOAS r h (x (x a) -> x a)

class BiFunctor r p where

Minimal complete definition

bimap

Methods

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

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)

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

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

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

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

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

app5 :: DBI r => r h (a4 -> a3 -> a2 -> a1 -> a -> b) -> r h a4 -> r h a3 -> r h a2 -> 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)

plus1 :: (Monoid * r a, DBI r) => r h a -> r h (a -> a)

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

module DDF.ImportMeta