Skip to content

Instantly share code, notes, and snippets.

@khibino

khibino/MetaTheory.agda

Last active Oct 17, 2020
Embed
What would you like to do?
Meta-Theory à la Carte using 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
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment