## Sunday, 4 January 2009

### beta eta equality for STLC by NbE

`{-# LANGUAGE NoMonomorphismRestriction #-}import Prelude hiding ((\$))import Control.Monadtype Ref = Intnewtype 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 jgamma |- 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 vdata V = VLam (V -> V)       | VNeutral Ndata N = NApp N V       | NQuote RefVLam f \$ x = f xVNeutral n \$ x = VNeutral (NApp n x)eval delta (Var j) = delta !! jeval 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)))------------------- NEWr :: T -> V -> Vr O e = er (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 nnq i (NApp m n) = App (nq i m) (q i n)nq i (NQuote j) = Quote jnf 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.Monadtype Ref = Intnewtype 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 vdata V = VLam T (V -> V) | VNeutral N       | VQuote Refdata N = NVar V | NApp N V       | NQuote Reflift 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 jeta 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 gammaetaReify O t delta gamma = betaEtaReify O t delta gammabetaEtaReify _   (Var i) delta gamma = delta !! ibetaEtaReify tau (Lam t (Scope b)) delta gamma = etaReify tau (Lam t (Scope b)) delta gammabetaEtaReify 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 nquote i (VQuote j) = Quote jnquote i (NVar v) = quote i vnquote i (NApp n v) = App (nquote i n) (quote i v)nquote i (NQuote j) = Quote jbetaEtaNF 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-}`