Meta-Theory à la Carte using Agda

MetaTheory.agda

-- Example implementation for Meta-Theory à la Carte

-- data Fix (f : Set -> Set) : Set where
--   inF : f (Fix f) -> Fix f

open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; _+_)
import Data.Nat as Nat

open import Data.Maybe using (Maybe; just; nothing)
open import Data.List using (List; []; _∷_)
open import Data.Product using (_×_; _,_)

open import Relation.Nullary using (yes; no)

---

Algebra : (Set -> Set) -> Set -> Set
Algebra f a = f a -> a

Fix : (Set -> Set) -> Set₁
Fix f = ∀ {a : Set} -> Algebra f a -> a

fold : ∀ {f a} -> Algebra f a -> Fix f -> a
fold alg fa = fa alg

---

AlgebraM : (Set -> Set) -> Set -> Set₁
AlgebraM f a = ∀{r : Set} -> (r -> a) -> f r -> a

FixM : (Set -> Set) -> Set₁
FixM f = ∀ {a : Set} -> AlgebraM f a -> a

foldM : ∀ {f a} -> AlgebraM f a -> FixM f -> a
foldM alg fa = fa alg

---

data _⨁_ (f : Set -> Set) (g : Set -> Set) (a : Set) : Set where
  Inl : f a -> (f ⨁ g) a
  Inr : g a -> (f ⨁ g) a

infixl 30 _⨁_

---

Env : Set -> Set
Env a = List (ℕ × a)

lookupEnv : {a : Set} -> Env a -> ℕ -> Maybe a
lookupEnv  []            n = nothing
lookupEnv ((n , x) ∷ ps) m with n Nat.≟ m
... | yes p = just x
... | no ¬p = nothing

---

data ArithF (a : Set) : Set where
  Lit : ℕ -> ArithF a
  Add : a -> a -> ArithF a

-- Arith : Set₁
-- Arith = Fix ArithF

data Value : Set where
  I : ℕ    -> Value
  B : Bool -> Value

-- evalArith : Algebra ArithF (Value ℕ)
evalArith : Algebra ArithF Value
evalArith (Lit n)   = I n
evalArith (Add (I n) (I m)) = I (n + m)
evalArith (Add (I _) (B _)) = I 0
evalArith (Add (B _) _)     = I 0

evalArithM : AlgebraM ArithF Value
evalArithM r (Lit n)    = I n
evalArithM r (Add n m) with r n
... | B x = I 0
... | I x with r m
... | I y = I (x + y)
... | B y = I 0

---

lit : ℕ -> Fix ArithF
lit n alg = alg (Lit n)

add : Fix ArithF -> Fix ArithF -> Fix ArithF
add e₁ e₂ alg = alg (Add (fold alg e₁) (fold alg e₂))

---

data LogicF (a : Set) : Set where
  If : a -> a -> a -> LogicF a
  BLit : Bool -> LogicF a

evalLogic : Algebra LogicF Value
evalLogic (If (B true)  v₁ v₂)  = v₁
evalLogic (If (B false) v₁ v₂)  = v₂
evalLogic (If (I _)     v₁ v₂)  = v₂
evalLogic (BLit b)              = B b

evalLogicM : AlgebraM LogicF Value
evalLogicM r (If b v₁ v₂) with r b
... | B true   = r v₁
... | B false  = r v₂
... | I _      = r v₂
evalLogicM _ (BLit b)     = B b

---

data LambdaF (a : Set) : Set where
  Var : ℕ -> LambdaF a
  Let : List (ℕ × a) -> a -> LambdaF a

postulate
  -- evalVar : {a : Set} -> List (ℕ × a) -> ℕ -> a
  substVars : {a : Set} -> List (ℕ × a) -> a -> a

evalLambdaM : AlgebraM LambdaF Value
evalLambdaM r (Var n)    = I 0
evalLambdaM r (Let ps e) = r (substVars ps e)

---

-- Exp : Set₁
-- Exp = FixM (ArithF ⨁ LogicF)
--   isomorphic to
-- data Exp = Lit Nat | Add Exp Exp | If Exp Exp Exp | BLit Bool

evalAlgPlus : ∀ {f g} -> AlgebraM f Value -> AlgebraM g Value -> AlgebraM (f ⨁ g) Value
evalAlgPlus af ag r (Inl fexp) = af r fexp
evalAlgPlus af ag r (Inr gexp) = ag r gexp

record Eval (f : Set -> Set) : Set₁ where
  field
    evalAlgR : AlgebraM f Value

mkEval : {f : Set -> Set} -> AlgebraM f Value -> Eval f
mkEval alg = record { evalAlgR = alg }

open Eval using (evalAlgR)

evalAlg : ∀ {f} -> {e : Eval f} -> AlgebraM f Value
evalAlg {e = e} = evalAlgR e

instance
  evalSum : ∀ {f g} -> {ef : Eval f} -> {eg : Eval g} -> Eval (f ⨁ g)
  evalSum {ef = ef} {eg = eg} = mkEval (evalAlgPlus (evalAlgR ef) (evalAlgR eg))

  evalArithF : Eval ArithF
  evalArithF = mkEval evalArithM

  evalLogicF : Eval LogicF
  evalLogicF = mkEval evalLogicM

  evalLambdaF : Eval LambdaF
  evalLambdaF = mkEval evalLambdaM

eval : ∀ {f} -> {e : Eval f} -> FixM f -> Value
eval {e = e} = foldM (evalAlgR e)

Exp : Set -> Set
Exp = ArithF ⨁ LogicF ⨁ LambdaF

evalExp : {Eval Exp} -> FixM Exp -> Value
evalExp {e} = eval {e = e}

-- evalX : FixM (ArithF ⨁ LogicF) -> Value
-- evalX = eval {_} {evalSum {_} {_} {evalArithF} {evalLogicF}}
-- evalX = eval {_} {evalSum}
-- evalX x = eval x

MetaTheory.hs

{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}

type Algebra f a = f a -> a

type Fix f = forall a . Algebra f a -> a

fold :: forall f a . Algebra f a -> Fix f -> a
fold alg fa = fa alg

---

type AlgebraM f a = forall r . (r -> a) -> f r -> a

type FixM f = forall a . AlgebraM f a -> a

foldM :: forall f a . AlgebraM f a -> FixM f -> a
foldM alg fa = fa alg

---

type Nat = Int

data ArithF a
  = Lit Int
  | Add a a

data Value
  = I Int
  | B Bool

evalArith :: Algebra ArithF Value
evalArith (Lit n) = I n
evalArith (Add (I n) (I m)) = I (n + m)

evalArithM :: AlgebraM ArithF Value
evalArithM r (Lit n) = I n
evalArithM r (Add n m) = case (r n, r m) of
  (I x, I y) -> I (x + y)

lit :: Nat -> Fix ArithF
lit n alg = alg (Lit n)

add :: Fix ArithF -> Fix ArithF -> Fix ArithF
add e1 e2 alg = alg (Add (fold alg e1) (fold alg e2))

---

data LogicF a
  = If a a a
  | BLit Bool

evalLogic :: Algebra LogicF Value
evalLogic (If (B True)  v1 v2) = v1
evalLogic (If (B False) v1 v2) = v2
evalLogic (BLit b)             = B b

evalLogicM :: AlgebraM LogicF Value
evalLogicM r (If b v1 v2) = case r b of
  B True             -> r v1
  B False            -> r v2
evalLogicM _ (BLit b) = B b

---

data (⨁) f g a
  = Inl (f a)
  | Inr (g a)

infixl 3 ⨁

---

class Eval f where
  evalAlg :: AlgebraM f Value

---

instance (Eval f, Eval g) => Eval (f ⨁ g) where
  evalAlg r (Inl fexp) = evalAlg r fexp
  evalAlg r (Inr gexp) = evalAlg r gexp

---

eval :: Eval f => FixM f -> Value
eval = foldM evalAlg