As a learning exercise, I decided to try to convert the ML code on the Wikipedia page for normalisation by evaluation into Haskell. The main barrier (or so I thought) was that the ML code mutates a variable in order to get a supply of fresh names. I thought I was going to easily get around this by using de Bruijn indices instead.
The Wikipedia page is, possibly, abandoned, since most of the sample implementation dates from 2007. So I am not sure whether I have bungled this translation of the code to Haskell, or if the code snippets on Wikipedia are buggy/incomplete/abandoned. Maybe somebody can advise me on a better source, or point out obvious inadequacies in the code.
data Ty = Basic String | Arrow Ty Ty | Prod Ty Ty
deriving Show
data Tm = Var Int | Lam Tm | App Tm Tm | Pair Tm Tm | Fst Tm | Snd Tm
deriving Show
data Sem = LAM (Sem -> Sem) | PAIR Sem Sem | SYN Tm
instance Show Sem where
show = showSem
showSem (LAM a) = "LAM (Func)"
showSem (PAIR s1 s2) = "PAIR" ++ show s1 ++ show s2
showSem (SYN tm) = "SYN" ++ show tm
reflect :: Ty -> Tm -> Sem
reflect (Arrow a b) t = LAM (\ ss -> reflect b (App t (reify a ss)))
reflect (Prod a b) t = PAIR (reflect a (Fst t)) (reflect b (Snd t))
reflect (Basic _) t = SYN t
reify :: Ty -> Sem -> Tm
reify (Arrow a b) (LAM s) = Lam (reify b (s (reflect a (Var 0))))
reify (Prod a b) (PAIR s t) = Pair (reify a s) (reify b t)
reify (Basic _) (SYN t) = t
type Ctx = [Sem]
nbe_lookup :: Ctx -> Int -> Sem
nbe_lookup g n = g !! n
meaning :: Ctx -> Tm -> Sem
meaning g t = case t of
Var x -> nbe_lookup g x
Lam s -> LAM (\ ss -> meaning (ss:g) s)
App s t -> case meaning g s of LAM ss -> ss (meaning g t)
Pair s t -> PAIR (meaning g s) (meaning g t)
Fst s -> (case meaning g s of (PAIR ss tt) -> ss)
Snd t -> (case meaning g t of (PAIR ss tt) -> tt)
nbe :: Ty -> Tm -> Tm
nbe a t = reify a (meaning [] t)
k = Lam (Lam (Var 1))
s = Lam (Lam (Lam (App (App (Var 2) (Var 0)) (App (Var 1) (Var 0)))))
skk = App (App s k) k
-- nbe (Arrow (Basic "a", Basic "a")) skk
I managed to track down the original author of the code on the Wikipedia page.
We had a discussion over email, and the conclusion is that the code on Wikipedia is fine, and ports easily to Haskell, but a de Bruijn approach is more complex than I had appreciated. He kindly provided the following Haskell version of the code from http://en.wikipedia.org/wiki/Normalisation_by_evaluation:
-- module WPNbe where
import Control.Monad.ST
import Data.STRef
data Ty = Basic Int
| Arrow Ty Ty
| Prod Ty Ty
deriving (Eq, Show)
data Tm = Var Int
| Lam Int Tm
| App Tm Tm
| Pair Tm Tm
| Fst Tm | Snd Tm
deriving (Eq, Show)
data Sem s = LAM (Sem s -> ST s (Sem s))
| PAIR (Sem s) (Sem s)
| SYN Tm
reflect :: STRef s Int -> Ty -> Tm -> Sem s
reflect k (Arrow a b) t =
LAM (\ ss -> do
v <- reify k a ss
pure $ reflect k b (App t v))
reflect k (Prod a b) t =
PAIR (reflect k a (Fst t)) (reflect k b (Snd t))
reflect k (Basic _) t = SYN t
reify :: STRef s Int -> Ty -> Sem s -> ST s Tm
reify k (Arrow a b) (LAM f) = do
n <- readSTRef k
writeSTRef k $ n + 1
let arg = reflect k a (Var n)
ss <- f arg
t <- reify k b ss
pure $ Lam n t
reify k (Prod a b) (PAIR ss tt) = do
s <- reify k a ss
t <- reify k b tt
pure $ Pair s t
reify k (Basic _) (SYN t) = pure t
type Cx s = [(Int, Sem s)]
find :: Cx s -> Int -> Sem s
find ((u, ss) : cx) x =
if u == x then ss else find cx x
initial :: Cx s -> Tm -> ST s (Sem s)
initial cx (Var x) = pure $ find cx x
initial cx (Lam x t) =
pure $ LAM (\ ss -> initial ((x, ss) : cx) t)
initial cx (App s t) = do
u <- initial cx s
v <- initial cx t
case u of
LAM f -> f v
initial cx (Pair s t) = do
u <- initial cx s
v <- initial cx t
pure $ PAIR u v
initial cx (Fst s) = do
u <- initial cx s
case u of
PAIR t _ -> pure t
initial cx (Snd s) = do
u <- initial cx s
case u of
PAIR _ t -> pure t
nbe :: Ty -> Tm -> Tm
nbe ty t = runST $ do
k <- newSTRef 0
ss <- initial [] t
reify k ty ss
-- Tests
kC :: Tm
kC = Lam 1 (Lam 2 (Var 1))
sC :: Tm
sC = Lam 1 (Lam 2 (Lam 3 (App (App (Var 1) (Var 3)) (App (Var 2) (Var 3)))))
skkC :: Tm
skkC = App (App sC kC) kC
main :: IO ()
main = do
putStrLn $ show $ nbe (Arrow (Basic 1) (Basic 1)) skkC
putStrLn $ show $ nbe (Arrow (Arrow (Basic 1) (Basic 2)) (Arrow (Basic 1) (Basic 2))) skkC
I think this is pretty clear in comparison to the other approaches mentioned in this thread. STRef is used to provide a supply of fresh variables.
