beta eta equality for STLC by NbE

{-# LANGUAGE NoMonomorphismRestriction #-}

import Prelude hiding (($))
import Control.Monad

type Ref = Int
newtype Scope a = Scope a deriving (Eq, Show)
data T = O | T :->: T deriving (Eq, Show)
data S = Var Ref | Lam T (Scope S) | App S S
       | Quote Ref deriving (Eq, Show)

abstract i t = Scope (extract 0 t) where
 extract r (Var j) = Var j
 extract r (Lam t (Scope b)) = Lam t (Scope (extract (r+1) b))
 extract r (App m n) = App (extract r m) (extract r n)
 extract r (Quote j)
  | j == i = Var r
  | otherwise = Quote j

gamma |- Var i = Just (gamma !! i)
gamma |- Lam u (Scope b) = do v <- (u:gamma) |- b ; return (u :->: v)
gamma |- App m n = do u :->: v <- gamma |- m ; u' <- gamma |- n ; guard (u == u') ; return v

data V = VLam (V -> V)
       | VNeutral N
data N = NApp N V
       | NQuote Ref

VLam f $ x = f x
VNeutral n $ x = VNeutral (NApp n x)

eval delta (Var j) = delta !! j
eval delta (Lam _ (Scope b)) = VLam (\x -> eval (x:delta) b)
eval delta (App m n) = eval delta m $ eval delta n

------------------- OLD
-- r :: T -> V -> V
-- r O e = e
-- r (tau :->: sigma) f = VLam (\x -> r sigma (f $ (r tau x)))

------------------- NEW
r :: T -> V -> V
r O e = e
r (tau :->: sigma) f = f $ VLam (\f -> r sigma (VLam (\x -> f $ (r tau x))))



q i (VLam f) = Lam O (abstract i (q (i+1) (f (VNeutral (NQuote i)))))
q i (VNeutral n) = nq i n

nq i (NApp m n) = App (nq i m) (q i n)
nq i (NQuote j) = Quote j

nf tm = fmap (q 0 . flip r (eval [] tm)) ([] |- tm)

identity = Lam (O :->: O) (Scope (Var 0))
dollar = Lam (O :->: O) (Scope (Lam O (Scope (App (Var 1) (Var 0)))))


{- OLDER
{-# LANGUAGE NoMonomorphismRestriction #-}

import Control.Monad

type Ref = Int
newtype Scope a = Scope a deriving (Eq, Show)
data T = O | T :->: T deriving (Eq, Show)
data S = Var Ref | Lam T (Scope S) | App S S
       | Quote Ref deriving (Eq, Show)

gamma |- Var i = Just (gamma !! i)
gamma |- Lam u (Scope b) = do v <- (u:gamma) |- b ; return (u :->: v)
gamma |- App m n = do u :->: v <- gamma |- m ; u' <- gamma |- n ; guard (u == u') ; return v

data V = VLam T (V -> V) | VNeutral N
       | VQuote Ref
data N = NVar V | NApp N V
       | NQuote Ref

lift i (Var j)
 | j < i = Var j
 | otherwise = Var (j+1)
lift i (Lam t (Scope b)) = Lam t (Scope (lift (i+1) b))
lift i (App m n) = App (lift i m) (lift i n)

abstract i t = Scope (extract 0 t) where
 extract r (Var j) = Var j
 extract r (Lam t (Scope b)) = Lam t (Scope (extract (r+1) b))
 extract r (App m n) = App (extract r m) (extract r n)
 extract r (Quote j)
  | j == i = Var r
  | otherwise = Quote j

eta u t = Lam u (Scope (App (lift 0 t) (Var 0)))

etaReify (u :->: v) (Lam t (Scope b)) delta gamma = VLam u (\x -> etaReify v b (x:delta) (u:gamma))
etaReify (u :->: v) t delta gamma = etaReify (u :->: v) (eta u t) delta gamma
etaReify O t delta gamma = betaEtaReify O t delta gamma

betaEtaReify _   (Var i) delta gamma = delta !! i
betaEtaReify tau (Lam t (Scope b)) delta gamma = etaReify tau (Lam t (Scope b)) delta gamma
betaEtaReify tau (App m n) delta gamma = app (betaEtaReify (sigma :->: tau) m delta gamma) (etaReify sigma n delta gamma)
 where sigma = case gamma |- n of Nothing -> error "Type error" ; Just sigma -> sigma
       app (VLam _ f) x = f x
       app (VNeutral n) x = VNeutral (NApp n x)
       app (VQuote j) x = VNeutral (NApp (NQuote j) x)

quote i (VLam t f) = Lam t (abstract i (quote (i+1) (f (VQuote i))))
quote i (VNeutral n) = nquote i n
quote i (VQuote j) = Quote j

nquote i (NVar v) = quote i v
nquote i (NApp n v) = App (nquote i n) (quote i v)
nquote i (NQuote j) = Quote j

betaEtaNF p = do
 t <- [] |- p
 return (quote 0 (etaReify t p [] []))

betaEtaEqual p q = do
 t <- [] |- p ; t' <- [] |- q ; guard (t == t')
 return (quote 0 (etaReify t p [] []) == quote 0 (etaReify t q [] []))

identity = Lam (O :->: O) (Scope (Var 0))
dollar = Lam (O :->: O) (Scope (Lam O (Scope (App (Var 1) (Var 0)))))

-- > betaEtaEqual identity dollar
-- Just True
-}