Implementation of evaluation without dynamic type casting in Syntactic

Binding.hs

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Syntactic



-- | Environment suffix relation
class Suff e s
  where
    suff :: e -> s

instance Suff e e
  where
    suff = id

instance (Suff e s, e' ~ (a,e)) => Suff e' s
  where
    suff = suff . snd

-- | Closure
newtype Cl e a = Cl {runCl :: e -> a}

data Binding a
  where
    Var :: (e -> a) -> Binding (Full (Cl e a))
    Lam :: Binding (Cl (a,e) b :-> Full (Cl e (a -> b)))
    Let :: Binding (Cl e a :-> Cl e (a -> b) :-> Full (Cl e b))

data Res a
  where
    Res :: {runRes :: a} -> Res (Full a)

class Eval s
  where
    evalSym :: s sig -> Args Res sig -> Res (Full (DenResult sig))

instance (Eval s, Eval t) => Eval (s :+: t)
  where
    evalSym (InjL s) = evalSym s
    evalSym (InjR s) = evalSym s

instance Eval Binding
  where
    evalSym (Var f) Nil                 = Res $ Cl f
    evalSym Lam (Res b :* Nil)          = Res $ Cl $ \e a -> runCl b (a,e)
    evalSym Let (Res a :* Res b :* Nil) = Res $ Cl $ \e -> runCl b e $ runCl a e

eval :: e -> Eval s => ASTF s (Cl e a) -> a
eval e = flip runCl e . runRes . fold evalSym

eval' :: Eval s => ASTF s (Cl () a) -> a
eval' = eval ()

type family   LiftCl e sig
type instance LiftCl e (Full a)    = Full (Cl e a)
type instance LiftCl e (a :-> sig) = Cl e a :-> LiftCl e sig

lowerRes :: Res (Full (Cl e a)) -> e -> Res (Full a)
lowerRes = (Res .) . runCl . runRes

lowerCl
    :: e
    -> Args c' sig
    -> Args Res (LiftCl e sig)
    -> Args Res sig
lowerCl _ Nil Nil              = Nil
lowerCl e (_ :* as') (a :* as) = lowerRes a e :* lowerCl e as' as

data Proxy a = Proxy

data ClSym s a
  where
    ClSym
        :: (DenResult (LiftCl e sig) ~ Cl e (DenResult sig))
        => Proxy e
        -> Args c' sig  -- To be able to reflect sig
        -> s sig
        -> ClSym s (LiftCl e sig)

instance Eval s => Eval (ClSym s)
  where
    evalSym (ClSym _ as' s) as = Res $ Cl $ \e -> runRes $ evalSym s $ lowerCl e as' as

data Arith a
  where
    Int :: Int -> Arith (Full Int)
    Add :: Num a => Arith (a :-> a :-> Full a)

instance Eval Arith
  where
    evalSym (Int i) Nil                 = Res i
    evalSym Add (Res a :* Res b :* Nil) = Res (a+b)

type Exp e a = ASTF (Binding :+: ClSym Arith) (Cl e a)

int :: Int -> Exp e Int
int = appSym . ClSym Proxy Nil . Int

(<+>) :: Num a => Exp e a -> Exp e a -> Exp e a
(<+>) = appSym (ClSym Proxy (Nothing :* Nothing :* Nil) Add)

var :: (e -> a) -> Exp e a
var f = appSym (Var f)

lam :: Exp (a,e) b -> Exp e (a -> b)
lam = appSym Lam

lett :: Exp e a -> Exp e (a -> b) -> Exp e b
lett = appSym Let

share :: forall e a b .
    Exp e a -> ((forall e' . Suff e' (a,e) => Exp e' a) -> Exp (a,e) b) -> Exp e b
share a f = lett a (lam $ f $ var $ \e -> fst (suff e :: (a,e)))

ex1   = int 2 <+> int 3
test1 = eval' ex1

ex2   = lett (int 3) (lam (var fst <+> var fst))
test2 = eval' ex2

ex3   = share (int 3 <+> int 4) $ \a -> a <+> a
test3 = eval' ex3

ex4   = share (int 3 <+> int 4) $ \a -> share (a <+> a) $ \b -> b <+> a
test4 = eval' ex4

Reference.hs

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}

class Suff e s
  where
    suff :: e -> s

instance Suff e e
  where
    suff = id

instance (Suff e s, e' ~ (a,e)) => Suff e' s
  where
    suff = suff . snd

data Exp e a
  where
    Var :: (e -> a) -> Exp e a
    Lam :: Exp (a,e) b -> Exp e (a -> b)
    App :: Exp e (a -> b) -> Exp e a -> Exp e b
    Int :: Int -> Exp e Int
    Add :: Num a => Exp e (a -> a -> a)

eval :: e -> Exp e a -> a
eval e (Var v)   = v e
eval e (Lam b)   = \a -> eval (a,e) b
eval e (App f a) = eval e f $ eval e a
eval e (Int i)   = i
eval e Add       = (+)

eval' :: Exp () a -> a
eval' = eval ()

(<+>) :: Num a => Exp e a -> Exp e a -> Exp e a
a <+> b = App (App Add a) b

share :: forall e a b .
    Exp e a -> ((forall e' . Suff e' (a,e) => Exp e' a) -> Exp (a,e) b) -> Exp e b
share a f = App (Lam $ f $ Var $ \e -> fst (suff e :: (a,e))) a

ex1   = Int 2 <+> Int 3
test1 = eval' ex1

ex2   = App (Lam (Var fst <+> Var fst)) (Int 3)
test2 = eval' ex2

ex3   = share (Int 3 <+> Int 4) $ \a -> a <+> a
test3 = eval' ex3

ex4   = share (Int 3 <+> Int 4) $ \a -> share (a <+> a) $ \b -> b <+> a
test4 = eval' ex4