An implementation of Martin-Löf's Logical Framework (MLF) with
dependent pairs using call-by-name weak head evaluation, untyped
conversion and bidirectional type-checking.

Author: Andreas Abel
Date  : Nov 2, 2004

\begin{code}
module MLFSigma where
import Prelude hiding (const, fst, snd)
import Data.FiniteMap
import Control.Monad.Error
\end{code}

Raw expressions.

\begin{code}
type Name = String
data Const = Set | El | Fun | Sig deriving Eq
data Exp   = Const Const | Var Name | Abs Name Exp | App Exp Exp 
           | Pair Exp Exp | Fst Exp | Snd Exp

set       = Const Set
el t      = Const El `App` t 
fun x a b = Const Fun `App` a `App` (Abs x b)
a ==> b   = fun "_" a b
sig x a b = Const Sig `App` a `App` (Abs x b)
prod a b  = sig "_" a b
\end{code}

Parameters, closures and values.

\begin{code}
type Par  = Int                               -- p
data Atom = Cst Const | Par Par deriving Eq   -- a
type Env  = FiniteMap Name Clos               -- rho
data Clos = Atom Par | Clos Exp Env           -- w
data Proj = L | R deriving Eq                 -- p
data Elim = FunE Clos | PairE Proj            -- e
\end{code}

Values are either neutral, i.e., an atom followed by a list of
eliminations, where the last elimination is the head of the list for
efficiency reasons.  Or, values are introductions.

\begin{code}
data Val  = Ne Atom [Elim] 
          | Lam Name Exp Env | Comma Exp Exp Env -- v

atom :: Atom -> Val
atom a = Ne a []

const :: Const -> Val
const c = atom (Cst c)

par :: Par -> Val
par p = atom (Par p)
\end{code}

Call-by-name weak head evaluation.  (Always succeeds if rho binds all vars.)

\begin{code}
eval :: Exp -> Env -> Val
eval (Const c)  rho = const c
eval (Var x)    rho = evalClos (lookupWithDefaultFM rho 
                                (error "unbound Var") x)
eval (Abs x t)  rho = Lam x t rho
eval (App r s)  rho = app (eval r rho) (Clos s rho)
eval (Pair r s) rho = Comma r s rho
eval (Fst r)    rho = fst (eval r rho)
eval (Snd r)    rho = snd (eval r rho)

app :: Val -> Clos -> Val
app (Ne a es) w     = Ne a (FunE w : es)
app (Lam x t rho) w = eval t (addToFM rho x w)
app _ _ = error "app: Not a function"

fst :: Val -> Val
fst (Ne a es) =      Ne a (PairE L : es)
fst (Comma r s rho) = eval r rho
fst _ = error "fst: Not a pair"

snd :: Val -> Val
snd (Ne a es) =      Ne a (PairE R : es)
snd (Comma r s rho) = eval s rho
snd _ = error "snd: Not a pair"

evalClos :: Clos -> Val
evalClos (Atom p)     = par p
evalClos (Clos t rho) = eval t rho
\end{code}

Monadic Bool.

\begin{code}
type Result a = Either String a
type MBool = Result ()

true  = return ()
false = fail ""

fromBool :: Bool -> MBool
fromBool b = if b then true else false

eq :: Eq a => a -> a -> MBool
eq x y = if (x == y) then true else fail "eq: no match"

allM :: (a -> MBool) -> [a] -> MBool
allM p = foldl (\ r a -> r >> p a) true

\end{code}

Untyped conversion.

\begin{code}
class GenSym a where
    genSym :: a -> (Par, a)

conv :: GenSym a => a -> Val -> Val -> Result ()
conv g v v' = conv' v v'

    where conv' :: Val -> Val -> Result ()

          conv' (Ne a es) (Ne a' es') = a `eq` a' >> allM convE (zip es es') 

          conv' v@(Lam _ _ _) v'@(Lam _ _ _) = conv g' (app v a) (app v' a)
          conv' v@(Lam _ _ _) v'@(Ne _ _   ) = conv g' (app v a) (app v' a)
          conv' v@(Ne _ _)    v'@(Lam _ _ _) = conv g' (app v a) (app v' a)

          conv' v@(Comma _ _ _) v'@(Comma _ _ _) = conv' (fst v) (fst v') >>
                                                   conv' (snd v) (snd v')
          conv' v@(Ne _ _)      v'@(Comma _ _ _) = conv' (fst v) (fst v') >>
                                                   conv' (snd v) (snd v')
          conv' v@(Comma _ _ _) v'@(Ne _ _)      = conv' (fst v) (fst v') >>
                                                   conv' (snd v) (snd v')

          (p,g') = genSym g
          a      = Atom p

          convE :: (Elim, Elim) -> Result ()
          convE (FunE w,  FunE w')  = conv' (evalClos w) (evalClos w')
          convE (PairE p, PairE p') = p `eq` p'
\end{code}

Contexts.

\begin{code}
newtype Counter = Counter Int

instance GenSym Counter where
    genSym (Counter k) = (k, Counter (k+1))

data Cxt = Cxt (FiniteMap Par Val) Counter

instance GenSym Cxt where
    genSym (Cxt cxt k) = (p, Cxt cxt k')
        where (p, k') = genSym k

empty :: Cxt
empty = Cxt emptyFM (Counter 0)

push :: Cxt -> Val -> (Cxt, Par)
push (Cxt cxt g) v = (Cxt cxt' g', p)
    where (p, g') = genSym g
          cxt'    = addToFM cxt p v

get :: Cxt -> Par -> Val
get (Cxt cxt g) p = lookupWithDefaultFM cxt (error "parameter not bound") p
\end{code}

Type checking.

\begin{code}
isType :: Cxt -> Exp -> Env -> MBool  -- Env is just a renaming

isType cxt (Const Set) rho = true

isType cxt ((Const El) `App` t) rho = check cxt t rho (const Set)

isType cxt (((Const Fun) `App` r) `App` (Abs x s)) rho = 
    isType cxt r rho >> isType cxt' s rho'
    where (cxt', p) = push cxt (eval r rho)
          rho'      = addToFM rho x (Atom p)

isType cxt (((Const Sig) `App` r) `App` (Abs x s)) rho = 
    isType cxt r rho >> isType cxt' s rho'
    where (cxt', p) = push cxt (eval r rho)
          rho'      = addToFM rho x (Atom p)

isType _ _ _ = fail ("isType: not a valid type")


check :: Cxt -> Exp -> Env -> Val -> Result ()

check cxt (Abs x t) rho (Ne (Cst Fun) [FunE f, FunE w]) = check cxt' t rho' fa
    where (cxt', p) = push cxt (evalClos w)
          a         = Atom p
          rho'      = addToFM rho x a
          fa        = evalClos f `app` a

check cxt (Pair r s) rho (Ne (Cst Sig) [FunE f, FunE w]) = 
    check cxt r rho (evalClos w) >>
    check cxt s rho (evalClos f `app` Clos r rho)

check cxt t rho v = 
    do v' <- infer cxt t rho
       conv cxt v v'

infer :: Cxt -> Exp -> Env -> Result Val

infer cxt (Var x) rho =
    case (lookupFM rho x) of
       Just (Atom p) -> return (get cxt p)
       _ -> fail ("infer: Variable " ++ x ++ " not bound")

infer cxt (App r s) rho =
    do v <- infer cxt r rho
       case v of
         (Ne (Cst Fun) [FunE f, FunE w]) -> 
             check cxt s rho (evalClos w) >>
             return (evalClos f `app` Clos s rho)
         _ -> fail ("infer: Not a function type")

infer cxt (Fst r) rho =
    do v <- infer cxt r rho
       case v of
         (Ne (Cst Sig) [FunE f, FunE w]) -> return (evalClos w)
         _ -> fail ("infer: Not a pair type")

infer cxt (Snd r) rho =
    do v <- infer cxt r rho
       case v of
         (Ne (Cst Sig) [FunE f, FunE w]) -> 
             return (evalClos f `app` Clos (Fst r) rho)
         _ -> fail ("infer: Not a pair type")


infer _ _ _ = fail ("infer: Not a neutral expression")
\end{code}

Top level.

\begin{code}
doit :: Exp -> Exp -> Result ()
doit e t = isType empty t emptyFM >> 
           check empty e emptyFM (eval t emptyFM)
\end{code}


Successful tests.

\begin{code}
t1 = doit (Abs "A" (Abs "x" (Var "x"))) 
       (fun "B" set (fun "y" (el (Var "B")) (el (Var "B"))))
t2 = doit (Abs "x" (Abs "x" (Var "x"))) 
       (fun "x" set (el (Var "x") ==> el (Var "x")))
t3 = doit (Abs "A" (Abs "B" (Abs "p" (Pair (Fst (Var "p")) (Snd (Var "p"))))))
       $ fun "A" set $ fun "B" set $ fun "p" (prod (el (Var "A")) (el (Var "B"))) $ prod (el (Var "A")) (el (Var "B"))
t4 = doit (Abs "A" (Abs "B" (Abs "p" (Pair (Fst (Var "p")) (Snd (Var "p"))))))
       $ fun "A" set $ fun "B" (el (Var "A") ==> set) $ fun "p" (sig "x" (el (Var "A")) (el (Var "B" `App` Var "x"))) $ sig "x" (el (Var "A")) (el (Var "B" `App` Var "x"))
t5 = doit (Abs "A" (Abs "B" (Abs "p" (Pair (Fst (Var "p")) (Snd (Var "p"))))))
       $ fun "A" set $ fun "B" (el (Var "A") ==> set) $ fun "p" (sig "x" (el (Var "A")) (el (Var "B" `App` Var "x"))) $ sig "y" (el (Var "A")) (el (Var "B" `App` Var "y"))
\end{code}

Failing tests.

\begin{code}
f1 = doit (Abs "x" (Var "x"))
       (fun "A" set (el (Var "A") ==> el (Var "A")))
f2 = doit set set
f3 = doit (Abs "A" (Abs "x" (Var "x"))) 
       (fun "B" set (fun "y" (el (Var "B")) (el (Var "C"))))
f4 = doit (Abs "A" (Abs "B" (Abs "p" (Pair (Fst (Var "p")) (Snd (Var "p"))))))
       $ fun "A" set $ fun "B" set $ fun "p" (prod (el (Var "A")) (el (Var "B"))) $ prod (el (Var "B")) (el (Var "A"))
f5 = doit (Abs "A" (Abs "B" (Abs "p" (Pair (Fst (Var "p")) (Snd (Var "p"))))))
       $ fun "A" set $ fun "B" (el (Var "A") ==> set) $ fun "p" (sig "x" (el (Var "A")) (el (Var "B" `App` Var "x"))) $ prod (el (Var "B")) (el (Var "A"))
f6 = doit (Abs "A" (Abs "B" (Abs "p" (Pair (Fst (Var "p")) (Snd (Var "p"))))))
       $ fun "A" set $ fun "B" (el (Var "A") ==> set) $ fun "p" (sig "x" (el (Var "A")) (el (Var "B" `App` Var "x"))) $ sig "x" (el (Var "A")) (el (Var "B" `App` Var "y"))
\end{code}