posts/how-to-keep-lambda-calculus-simple

[giscus[bot]]

posts/how-to-keep-lambda-calculus-simple

https://hirrolot.github.io/posts/how-to-keep-lambda-calculus-simple.html

[tromp]

Thanks for this most elucidating writeup, Hirrolot!

The following lines
iEval (Free x) d = case lookup x (fst d) of Nothing -> (vfree x); Just v -> v
iEval (Bound ii) d = (snd d) !! ii
cEval (Lam e) d = VLam (\x -> cEval e ((((e, d) -> (e, (x : d))) d)))

can be written more idiomatically/clearly as

iEval (Free x) (d,) = case lookup x d of Nothing -> (vfree x); Just v -> v
iEval (Bound ii) (,d) = d !! ii
cEval (Lam e) (d1,d2) = VLam (\x -> cEval e (d1, (x : d2)))

The lovely K combinator example is missing an Inf:

quote 0 (VLam (\x -> VLam (\y -> x)))
Lam (quote 1 (VLam (\y -> vfree (Quote 0))))
Lam (Lam (quote 2 (vfree (Quote 0))))
Lam (Lam (quote 2 (VNeutral (NFree (Quote 0)))))
Lam (Lam (Inf (neutralQuote 2 (NFree (Quote 0)))))
Lam (Lam (Inf (boundfree 2 (Quote 0))))
Lam (Lam (Inf (Bound 1)))

[hirrolot]

Thanks for your comment! 1) I copy-pasted the implementation from the linked article, this is why it's not as clean as it could be. 2) Nice catch, fixed.