{-# LANGUAGE MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, FlexibleInstances, FlexibleContexts, UndecidableInstances, PolyKinds, LambdaCase, NoMonomorphismRestriction, TypeFamilies, LiberalTypeSynonyms, FunctionalDependencies, ExistentialQuantification, InstanceSigs, ConstraintKinds, DefaultSignatures, TypeOperators, TypeApplications, PartialTypeSignatures, NoImplicitPrelude #-} module DDF.DBI (module DDF.DBI, module DDF.ImportMeta) where import DDF.ImportMeta class Monoid r m where zero :: r h m plus :: r h (m -> m -> m) class DBI (r :: * -> * -> *) where 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 -- | 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. hoas :: (r (a, h) a -> r (a, h) b) -> r h (a -> b) hoas f = abs $ f z com :: r h ((b -> c) -> (a -> b) -> (a -> c)) com = lam3 $ \f g x -> app f (app g x) flip :: r h ((a -> b -> c) -> (b -> a -> c)) flip = lam3 $ \f b a -> app2 f a b id :: r h (a -> a) id = lam $ \x -> x const :: r h (a -> b -> a) const = lam2 $ \x _ -> x scomb :: r h ((a -> b -> c) -> (a -> b) -> (a -> c)) scomb = lam3 $ \f x arg -> app2 f arg (app x arg) dup :: r h ((a -> a -> b) -> (a -> b)) dup = lam2 $ \f x -> app2 f x x let_ :: r h (a -> (a -> b) -> b) let_ = flip1 id class LiftEnv r where liftEnv :: r () a -> r h a const1 = app const map2 = app2 map return = pure bind2 = app2 bind map1 = app map join1 = app join bimap2 = app2 bimap bimap3 = app3 bimap flip1 = app flip flip2 = app2 flip let_2 = app2 let_ class DBI r => Functor r f where map :: r h ((a -> b) -> (f a -> f b)) class Functor r a => Applicative r a where pure :: r h (x -> a x) ap :: r h (a (x -> y) -> a x -> a y) class Applicative r m => Monad r m where bind :: r h (m a -> (a -> m b) -> m b) join :: r h (m (m a) -> m a) join = lam $ \m -> bind2 m id bind = lam2 $ \m f -> join1 (app2 map f m) {-# MINIMAL (join | bind) #-} class BiFunctor r p where bimap :: r h ((a -> b) -> (c -> d) -> p a c -> p b d) com2 = app2 com class NT repr l r where conv :: repr l t -> repr r t class NTS repr l r where convS :: repr l t -> repr r t instance (DBI repr, NT repr l r) => NTS repr l (a, r) where convS = s . conv instance {-# OVERLAPPABLE #-} NTS repr l r => NT repr l r where conv = convS instance {-# OVERLAPPING #-} NT repr x x where conv x = x 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) lam f = hoas (\x -> f $ conv x) 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) lam2 f = lam $ \x -> lam $ \y -> f x y lam3 f = lam2 $ \a b -> lam $ \c -> f a b c lam4 f = lam3 $ \a b c -> lam $ \d -> f a b c d app2 f a = app (app f a) app3 f a b = app (app2 f a b) app4 f a b c = app (app3 f a b c) app5 f a b c d = app (app4 f a b c d) plus2 = app2 plus noEnv :: repr () x -> repr () x noEnv x = x scomb2 = app2 scomb plus1 = app plus dup1 = app dup