abt.hs

-- 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)

lambda.hs

-- 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"