Trying to implement normalisation by evaluation, based on the Wikipedia page

Learn
#1

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
1 Like
#2

@david-christiansen has written a tutorial on using NbE in Haskell that you might want to check out: https://davidchristiansen.dk/tutorials/implementing-types-hs.pdf

1 Like
#3

Thanks, I have that but got bogged down with it. Also out there are the papers and implementations on the (newish?) PLS Wiki:
https://www.pls-lab.org/en/Normalization_by_Evaluation

#4

I can recommend GitHub - AndrasKovacs/elaboration-zoo: Minimal implementations for dependent type checking and elaboration as a good (and working!) Haskell exposition to NBE both with and without typechecking

2 Likes
#5

From ~6:30 in this video, Ed live-codes a NbE interpreter that might be easier to follow:

3 Likes
#6

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.

As far as getting de Bruijn indices/de Bruijn levels to work goes, Iā€™m looking at implementation - When should I use De Bruijn levels instead of indices? - Proof Assistants Stack Exchange.