Zhixuan Yang

@maxsnew@types.pl there is one person to blame who popularised monads as a user-facing programming construct, which has resulted in the unfortunate reputation of Haskell as an esoteric mathematical programming language, among some other unfortunate consequences...

Just edited the post because I came up with the right way to lazy shifting of de Bruijn indices for the very last normaliser (apart from using freshly named variables that @AndrasKovacs told me yesterday). Also fixed a strictness bug. I had to duplicate the definition of some functions only for different strictness/laziness annotations. Is "strictness polymorphism" a thing?

@maxsnew@types.pl Sorry I realised my last response wasn't about the algebraic effects vs monads false comparison, but the effect handler vs monads false comparison, which has hurt me more.

@AndrasKovacs thanks so much for the pointers! I am quite ignorant about the existing literature on efficient normalisation so these pointers are extremely useful to me

@DDOtten Thank you so much for the feedback! I am very happy to know you liked the post!

I think your nf8 computes the normal form correctly, but I am worrying about the cost when arguments are repetitively reified. When you cache the normal form of an argument, shift 0 i is applied to the normal form, but the normal form may become a part of the normal form of another argument, which needs reification and shift 0 again.

In particularly, for the following term

-- t = (\x. \y. y x) ((\x. \y. y x) (...))
t :: Int -> Tm
t 0 = Abs (Var 0)
t n = Abs (Abs (Var 0 `App` Var 1)) `App` t (n-1)

where the cached normal form of the argument contains the cached normal form of the argument of the cached normal form of the argument.... nf8 is slow on my machine:

-- >>> fv (nf8 (t 10000))

but nf5 is fast:

-- >>> fv (nf5 (t 10000)) -- -1

(By the way, embarrassingly, the updated nf7 in the current version of my post is in fact incorrect... I am still thinking about if it can be saved...)