Minimal environment machine normalization with a fixpoint operator

FixNf.hs

{-# language Strict, BangPatterns #-}

data Tm = Var Int | App Tm Tm | Lam Tm | Fix Tm deriving (Show, Eq)
data Val = VVar Int | VApp Val Val | VLam [Val] Tm | VFix [Val] Tm

isCanonical :: Val -> Bool
isCanonical VLam{} = True
isCanonical _      = False

eval :: [Val] -> Tm -> Val
eval vs (Var x)   = vs !! x
eval vs (App t u) = case (eval vs t, eval vs u) of
                      (VLam vs t, !u)                 -> eval (u:vs) t
                      (VFix vs t,  u) | isCanonical u -> eval (u:VFix vs t:vs) t
                      (t,          u)                 -> VApp t u
eval vs (Lam t)   = VLam vs t
eval vs (Fix t)   = VFix vs t

quote :: Int -> Val -> Tm
quote l (VVar x)    = Var (l - x - 1)
quote l (VApp t u)  = App (quote l t) (quote l u)
quote l (VLam vs t) = Lam (quote (l + 1) (eval (VVar l:vs) t))
quote l (VFix vs t) = Fix (quote (l + 2) (eval (VVar (l+1):VVar l:vs) t))

nf :: Tm -> Tm
nf = quote 0 . eval []

-- examples
------------------------------------------------------------

instance Num Tm where
  fromInteger = Var . fromInteger
  (+) = undefined; (*) = undefined
  abs = undefined; signum = undefined; (-) = undefined

($$) = App
infixl 7 $$

-- Church natural numbers
z   = Lam $ Lam $ 0
s   = Lam $ Lam $ Lam $ 1 $$ (2 $$ 1 $$ 0)
add = Lam $ Lam $ Lam $ Lam $ 3 $$ 1 $$ (2 $$ 1 $$ 0)
mul = Lam $ Lam $ Lam $ Lam $ 3 $$ (2 $$ 1) $$ 0

n5   = s $$ (s $$ (s $$ (s $$ (s $$ z))))
n10  = add $$ n5 $$ n5
n100 = mul $$ n10 $$ n10

-- Scott naturals
z' = Lam $ Lam $ 0
s' = Lam $ Lam $ Lam $ 1 $$ 2

-- recursive Scott addition
-- add' = fix rec a. case a of
--          S a' -> \b. S (rec a' b)
--          Z    -> \b.b

add'  = Fix $ 0 $$ (Lam $ Lam $ s' $$ (3 $$ 1 $$ 0)) $$ (Lam $ 0)
n5'   = s' $$ (s' $$ (s' $$ (s' $$ (s' $$ z'))))
n10'  = add' $$ n5' $$ n5'
n20'  = add' $$ n10' $$ n10'

-- recursive Scott-to-Church conversion
-- s2c = fix rec a. case a of
--         S a' -> s (rec a')
--         Z    -> z

s2c = Fix $ 0 $$ (Lam $ s $$ (2 $$ 0)) $$ z

test :: Bool
test = nf (s2c $$ n10') == nf n10

Ah, now I see it. So basically, we only evaluate Fix when we know that it's applied to an argument that can determine control flow (by some computation on it), so as to not unfold inner recursive calls indefinitely. Thanks for the explanation!