Created
August 4, 2012 16:46
-
-
Save ekmett/3258737 to your computer and use it in GitHub Desktop.
remote dsl
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE GADTs, Rank2Types, KindSignatures, ScopedTypeVariables, TypeOperators, DataKinds, PolyKinds, MultiParamTypeClasses, FlexibleInstances, TypeFamilies, DoRec, ExtendedDefaultRules #-} | |
import Control.Applicative | |
import Control.Category | |
import Control.Comonad | |
import Control.Monad.Fix | |
import Control.Monad (ap) | |
import Data.Functor.Identity | |
import Data.Typeable | |
import Data.Monoid | |
import Data.Unique | |
import System.IO.Unsafe | |
import Unsafe.Coerce | |
import Prelude hiding ((.),id) | |
infixl 1 >>>-, >>- | |
type Nat f g = forall x. f x -> g x | |
class HFunctor t where | |
hmap :: Nat f g -> Nat (t f) (t g) | |
class HFunctor t => HTraversable t where | |
htraverse :: Applicative m => (forall x. f x -> m (g x)) -> t f a -> m (t g a) | |
class HFunctor t => HMonad t where | |
hreturn :: Nat f (t f) | |
(>>-) :: t f a -> Nat f (t g) -> t g a | |
infixr 1 -<< | |
(-<<) :: HMonad t => Nat f (t g) -> Nat (t f) (t g) | |
f -<< m = m >>- f | |
class HBound s where | |
(>>>-) :: HMonad t => s t f a -> Nat f (t g) -> s t g a | |
class HMonadTrans s where | |
hlift :: HMonad t => Nat (t f) (s t f) | |
data Var b f a where | |
B :: b a -> Var b f a | |
F :: f a -> Var b f a | |
instance HFunctor (Var b) where | |
hmap _ (B b) = B b | |
hmap f (F a) = F (f a) | |
instance HTraversable (Var b) where | |
htraverse _ (B b) = pure (B b) | |
htraverse f (F a) = F <$> f a | |
instance HMonad (Var b) where | |
hreturn = F | |
B b >>- _ = B b | |
F a >>- f = f a | |
newtype Scope b t f a = Scope { unscope :: t (Var b (t f)) a } | |
instance HFunctor t => HFunctor (Scope b t) where | |
hmap f (Scope b) = Scope (hmap (hmap (hmap f)) b) | |
instance HTraversable t => HTraversable (Scope b t) where | |
htraverse f (Scope b) = Scope <$> htraverse (htraverse (htraverse f)) b | |
instance HMonad t => HMonad (Scope b t) where | |
hreturn = Scope . hreturn . F . hreturn | |
Scope e >>- f = Scope $ e >>- \v -> case v of | |
B b -> hreturn (B b) | |
F ea -> ea >>- unscope . f | |
instance HMonadTrans (Scope b) where | |
hlift = Scope . hreturn . F | |
instance HBound (Scope b) where | |
Scope m >>>- f = Scope (hmap (hmap (>>- f)) m) | |
data Equal a b where | |
Refl :: Equal a a | |
instance Category Equal where | |
id = Refl | |
Refl . Refl = Refl | |
abstract :: HMonad t => (forall x. f x -> Maybe (b x)) -> Nat (t f) (Scope b t f) | |
abstract f = Scope . hmap (\y -> case f y of | |
Just b -> B b | |
Nothing -> F (hreturn y)) | |
instantiate :: HMonad t => Nat b (t f) -> Nat (Scope b t f) (t f) | |
instantiate k (Scope e) = e >>- \v -> case v of | |
B b -> k b | |
F a -> a | |
data Ix :: [*] -> * -> * where | |
Z :: Ix (a ': as) a | |
S :: Ix as b -> Ix (a ': as) b | |
data Vec :: (* -> *) -> [*] -> * where | |
HNil :: Vec f '[] | |
(:::) :: f b -> Vec f bs -> Vec f (b ': bs) | |
infixr 5 :++, ::: | |
type family (:++) (as :: [*]) (bs :: [*]) :: [*] | |
type instance '[] :++ bs = bs | |
type instance (a ': as) :++ bs = a ': (as :++ bs) | |
happend :: Vec f as -> Vec f bs -> Vec f (as :++ bs) | |
happend HNil bs = bs | |
happend (a ::: as) bs = a ::: happend as bs | |
hsingleton :: f a -> Vec f '[a] | |
hsingleton x = x ::: HNil | |
instance HFunctor Vec where | |
hmap _ HNil = HNil | |
hmap f (x ::: xs) = f x ::: hmap f xs | |
instance HTraversable Vec where | |
htraverse _ HNil = pure HNil | |
htraverse f (x ::: xs) = (:::) <$> f x <*> htraverse f xs | |
class EqF f where | |
(==?) :: f a -> f b -> Maybe (Equal a b) | |
data Lit t where | |
Integer :: Integer -> Lit Integer | |
Double :: Double -> Lit Double | |
String :: String -> Lit String | |
value :: Lit a -> a | |
value (Integer i) = i | |
value (Double d) = d | |
value (String s) = s | |
class Literal a where | |
literal :: a -> Lit a | |
instance Literal Integer where | |
literal = Integer | |
instance Literal String where | |
literal = String | |
data Remote :: (* -> *) -> * -> * where | |
Var :: f a -> Remote f a | |
Lit :: Lit a -> Remote f a | |
Lam :: Scope (Equal b) Remote f a -> Remote f (b -> a) | |
Let :: Vec (Scope (Ix bs) Remote f) bs -> Scope (Ix bs) Remote f a -> Remote f a | |
Ap :: Remote f (a -> b) -> Remote f a -> Remote f b | |
lam_ :: EqF f => f a -> Remote f b -> Remote f (a -> b) | |
lam_ v f = Lam (abstract (v ==?) f) | |
lit :: Literal a => a -> Remote f a | |
lit = Lit . literal | |
instance HFunctor Remote where | |
hmap f (Var a) = Var (f a) | |
hmap _ (Lit t) = Lit t | |
hmap f (Lam b) = Lam (hmap f b) | |
hmap f (Let bs b) = Let (hmap (hmap f) bs) (hmap f b) | |
hmap f (Ap x y) = Ap (hmap f x) (hmap f y) | |
instance HTraversable Remote where | |
htraverse f (Var a) = Var <$> f a | |
htraverse _ (Lit t) = pure $ Lit t | |
htraverse f (Lam b) = Lam <$> htraverse f b | |
htraverse f (Let bs b) = Let <$> htraverse (htraverse f) bs <*> htraverse f b | |
htraverse f (Ap x y) = Ap <$> htraverse f x <*> htraverse f y | |
instance HMonad Remote where | |
hreturn = Var | |
Var a >>- f = f a | |
Lit t >>- _ = Lit t | |
Lam b >>- f = Lam (b >>>- f) | |
Let bs b >>- f = Let (hmap (>>>- f) bs) (b >>>- f) | |
Ap x y >>- f = Ap (x >>- f) (y >>- f) | |
(!) :: Vec f v -> Ix v a -> f a | |
(b ::: _) ! Z = b | |
(_ ::: bs) ! S n = bs ! n | |
eval :: Remote Identity a -> a | |
eval (Var w) = extract w | |
eval (Lit i) = value i | |
eval (Lam b) = \a -> eval (instantiate (\Refl -> Var (Identity a)) b) | |
eval (Let bs b) = eval (instantiate (vs !) b) where vs = hmap (instantiate (vs !)) bs | |
eval (Ap x y) = eval x (eval y) | |
closed :: HTraversable t => t f a -> Maybe (t g a) | |
closed = htraverse (const Nothing) | |
newtype V (a :: *) = V Unique | |
instance EqF V where | |
V a ==? V b | |
| a == b = Just (unsafeCoerce Refl) | |
| otherwise = Nothing | |
lam :: (Remote V a -> Remote V b) -> Remote V (a -> b) | |
lam f = unsafePerformIO $ do | |
x <- fmap V newUnique | |
return $ Lam $ abstract (x ==?) $ f $ Var x | |
data Binding a = V a := Remote V a | |
rhs :: Binding a -> Remote V a | |
rhs (_ := a) = a | |
data Bindings = forall bs. Bindings (Vec Binding bs) | |
elemIndex :: Vec Binding bs -> V a -> Maybe (Ix bs a) | |
elemIndex HNil _ = Nothing | |
elemIndex ((x := r) ::: xs) y = case x ==? y of | |
Just Refl -> Just Z | |
Nothing -> S <$> elemIndex xs y | |
instance Monoid Bindings where | |
mempty = Bindings HNil | |
Bindings xs `mappend` Bindings ys = Bindings (happend xs ys) | |
-- Allow the use of DoRec to define let statements | |
newtype Def a = Def { runDef :: IO (a, Bindings) } | |
instance Functor Def where | |
fmap f (Def m) = Def $ do | |
(a,w) <- m | |
return (f a, w) | |
instance Applicative Def where | |
pure = return | |
(<*>) = ap | |
instance Monad Def where | |
return a = Def $ return (a, mempty) | |
Def m >>= f = Def $ do | |
(a, xs) <- m | |
(b, ys) <- runDef (f a) | |
return (b, xs <> ys) | |
instance MonadFix Def where | |
mfix m = Def $ mfix $ \ ~(a, _) -> runDef (m a) | |
def :: Remote V a -> Def (Remote V a) | |
def v@Var{} = Def $ return (v, mempty) -- this thing already has a name | |
def r = Def $ do | |
v <- fmap V newUnique | |
return (Var v, Bindings (hsingleton (v := r))) | |
let_ :: Def (Remote V a) -> Remote V a | |
let_ (Def m) = unsafePerformIO $ do | |
(r, Bindings bs) <- m | |
return $ Let (hmap (abstract (elemIndex bs) . rhs) bs) | |
(abstract (elemIndex bs) r) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment