-
-
Save yfyf/ee56977d96db691b6087 to your computer and use it in GitHub Desktop.
This file contains hidden or 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
-- A port of: http://semantic-domain.blogspot.com/2015/03/abstract-binding-trees.html | |
{-# LANGUAGE DeriveFunctor #-} | |
module ABT where | |
import qualified Data.Foldable as Foldable | |
import Data.Foldable (Foldable) | |
import Data.Set (Set) | |
import qualified Data.Set as Set | |
import Prelude hiding (abs) | |
type V = String | |
data ABT f a | |
= Var V | |
| Abs V a | |
| Tm (f a) deriving (Functor, Show) | |
--instance Functor f => Functor (ABT f) where | |
-- fmap f abt = case abt of | |
-- Var x -> Var x | |
-- Abs v a -> Abs v (f a) | |
-- Tm t -> Tm (fmap f t) | |
data Term f = | |
Term { freevars :: Set V | |
, out :: ABT f (Term f) } | |
var :: V -> Term f | |
var v = Term (Set.singleton v) (Var v) | |
abs :: V -> Term f -> Term f | |
abs v body = Term (Set.delete v (freevars body)) (Abs v body) | |
tm :: (Foldable f, Functor f) => f (Term f) -> Term f | |
tm t = Term (Set.unions (Foldable.toList (fmap freevars t))) | |
(Tm t) | |
into :: (Foldable f, Functor f) => ABT f (Term f) -> Term f | |
into abt = case abt of | |
Var x -> var x | |
Abs v a -> abs v a | |
Tm t -> tm t | |
fresh :: (V -> Bool) -> V -> V | |
fresh used v | used v = fresh used ("'" ++ v) | |
fresh _ v = v | |
fresh' :: Set V -> V -> V | |
fresh' vs v = fresh (\v -> Set.member v vs) v | |
rename :: (Foldable f, Functor f) => V -> V -> Term f -> Term f | |
rename old new (Term fvs t) = case t of | |
Var v -> if v == old then var new else var old | |
Abs v body -> if v == old then abs v body | |
else abs v (rename old new body) | |
Tm v -> tm (fmap (rename old new) v) | |
-- | `subst t x body` substitutes `t` for `x` in `body`, avoiding capture | |
subst :: (Foldable f, Functor f) => Term f -> V -> Term f -> Term f | |
subst t x body = case out body of | |
Var v | x == v -> t | |
Var v -> var v | |
Abs x e -> abs x' e' | |
where memberOf s1 s2 v = Set.member v s1 || Set.member v s2 | |
x' = fresh (memberOf (freevars t) (freevars body)) x | |
-- rename x to something that cannot be captured | |
e' = if x /= x' then subst t x (rename x x' e) | |
else subst t x e | |
Tm body -> tm (fmap (subst t x) body) |
This file contains hidden or 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
-- A port of: http://semantic-domain.blogspot.com/2015/03/abstract-binding-trees.html | |
module Lambda where | |
import ABT | |
import Data.Foldable | |
import Data.Monoid (mappend) | |
data Tp = Base | Arrow Tp Tp | |
deriving (Eq,Show) | |
data T a | |
= Lam a | |
| App a a | |
| Let a a | |
| Ann Tp a | |
deriving (Show) | |
instance Functor T where | |
fmap f t = case t of | |
(Lam x) -> Lam (f x) | |
(App x y) -> App (f x) (f y) | |
(Let x y) -> Let (f x) (f y) | |
(Ann t x) -> Ann t (f x) | |
instance Foldable T where | |
foldMap f (Lam x) = f x | |
foldMap f (App x y) = f x `mappend` f y | |
foldMap f (Let x y) = f x `mappend` f y | |
foldMap f (Ann t x) = f x | |
type Ctx = [(V, Tp)] | |
is_synth (Tm (Lam _)) = False | |
is_synth (Tm (Let _ _)) = False | |
is_synth _ = True | |
is_check = not . is_synth | |
unabs e = | |
case (out e) of | |
Abs x e' -> (x, e') | |
_ -> error "Tried to unabs a non Abs" | |
check ctx e tp = | |
case (out e, tp) of | |
(Tm (Lam t), Arrow tp1 tp') -> | |
let (x, e') = unabs t in | |
check ((x, tp1):ctx) e' tp' | |
(Tm (Lam _), _) -> error "Expected arrow type" | |
(Tm (Let e' t), _) -> | |
let (x, e'') = unabs t in | |
let tp1 = synth ctx e' in | |
check ((x, tp1):ctx) e'' tp | |
(body, _) | is_synth body -> | |
case (tp == synth ctx e) of | |
True -> () | |
False -> error "Type mismatch" | |
_ -> | |
error "Invalid check case" | |
synth ctx e = | |
case (out e) of | |
Var x -> | |
case (lookup x ctx) of | |
Just t -> t | |
Nothing -> error "Unbound variable" | |
Tm (Ann tp e) -> | |
let () = check ctx e tp in tp | |
Tm (App f e) -> | |
case (synth ctx f) of | |
Arrow tp tp' -> | |
let () = check ctx e tp in tp | |
_ -> | |
error "Applying a non-function!" | |
body | is_check body -> | |
error $ "Cannot synthesize type for checking term" | |
p -> | |
error $ "Invalid synth case" | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment