Implementing the lambda calculus is, along with buying shoes and then not wearing them, one of my worse habits. Here’s today’s cookery, in literate Haskell. I’m using a certain amount of jiggery pokery.
> {-# LANGUAGE GADTs, KindSignatures, EmptyDataDecls,
> FlexibleInstances, FlexibleContexts
> #-}
I haven’t implemented weak normalization for a while, but Pierre Boutillier and I are currently experimenting with it, reviving my curiosity.
> module Wnf where > import Control.Applicative > import Data.Traversable > import Data.Foldable
Here come all the variations on terms, at once!
> data Form -- reducible stuff or only normal? > = Rdu | Nrm > data Stage -- syntax or internal semantic stuff? > = Syn Form | Sem > data Direction -- checking or inferring types? > = Chk | Inf
I’m pretending I have dependent types. It could be worse. Terms are indexed by stage, with syntactic representations for reducible terms and normal forms, and a “semantic” stage for weak normal forms. As ever, I keep parametric in the representation of parameters.
> data Tm :: {-Stage-}* -> {-Direction-}* -> * -> * where
First, the checkable stuff, for all stages.
> -- functions > F :: Bnd k x -> Tm k Chk x > -- canonical things > (:-) :: Con -> [Tm k Chk x] -> Tm k Chk x > -- noncanonical things > N :: Tm k Inf x -> Tm k Chk x
Next, the inferrable stuff, likewise.
> -- parameters > X :: x -> Tm k Inf x > -- eliminations (of noncanonical stuff) > (:$) :: Tm k Inf x -> Elim (Tm k Chk x) -> Tm k Inf x > -- operations > (:@) :: Op -> [Tm k Chk x] -> Tm k Inf x
Syntactic forms are permitted to use de Bruijn indices.
> V :: Int -> Tm (Syn a) Inf x
Syntactic, reducible forms may have definitions and type annotations.
> (:=:) :: Tm (Syn Rdu) Inf x -> Bnd (Syn Rdu) x -> > Tm (Syn Rdu) Chk x > (:::) :: Tm (Syn Rdu) Chk x -> Tm (Syn Rdu) Chk x -> > Tm (Syn Rdu) Inf x
Now, what’s a binding? A syntactic scope is indicated thus, carrying name advice, but really marking a shift in de Bruijn indexing, with the bound variable being (V 0).
> data Sc t = String :. t
With this to hand, we can now say how to bind a variable at any given stage. You may always write a vacuous binder with K (no de Bruijn shift!). However, non-vacuous binders are your regular lambda in the syntax, but closures in the semantics — terms packed with an environment that’s waiting with one empty slot!
> data Bnd :: {-Stage-}* -> * -> * where
> K :: Tm k Chk x -> Bnd k x
> L :: Sc (Tm (Syn a) Chk x) -> Bnd (Syn a) x
> C :: Sc (Tm (Syn a) Chk x) -> [Val x] -> Bnd Sem x
What’s a value? You’ve seen them already!
> type Val = Tm Sem Chk
Given a value, we can instantiate a binding. This can kick off some more weak normalization, filling in the empty slot in the closure.
> inst :: Bnd Sem x -> Val x -> Val x > inst (K r) _ = r > inst (C (_ :. t) g) v = wnf t (v : g)
What’s weak normalization? We can turn anything syntactic into a weak normal form, given an environment (idiomatically).
> wnf :: Tm (Syn a) k x -> [Val x] -> Val x > wnf (c :- ts) = (c :-) < $> traverse wnf ts > wnf (F (K t)) = (F . K) < $> wnf t > wnf (F (L s)) = F < $> C s -- make a closure! > wnf (N t) = wnf t > wnf (X x) = pure (N (X x)) > wnf (t :$ e) = ($$) < $> wnf t < *> traverse wnf e > wnf (o :@ ts) = (o @@) < $> traverse wnf ts > wnf (V i) = (!! i) > wnf (s :=: K t) = wnf t > wnf (s :=: L (_ :. t)) = \g -> wnf t (wnf s g : g) > wnf (t ::: _) = wnf t
I haven’t really built a type system yet, but I can tell I’ll want some canonical constructors, including one for making tuples.
> data Con = Set | Pi | Sig | Struct | Tup deriving Show
Meanwhile, I expect I’ll need function application and projection as elimination forms, with the semantics given below:
> data Elim t > = A t > | HD | TL > ($$) :: Val x -> Elim (Val x) -> Val x > N n $$ e = N (n :$ e) -- constipation > F b $$ A v = inst b v -- computation > (Tup :- (v : _)) $$ HD = v > (Tup :- (_ : vs)) $$ TL = Tup :- vs
Operator later, mater!
> data Op > instance Show Op where > show _ = "wow!" > (@@) :: Op -> [Val x] -> Val x > o @@ vs = N (o :@ vs)
Now let’s go from semantics back to syntax — from weak normal forms to normal forms. Without any type information, we can at least do beta.
What we need is a notion of parameter which allows us to generate fresh names, and to recognize when a name has been introduced locally, yielding a de Bruijn index. It’s my usual tumble between de Bruijn levels and de Bruijn indices.
> class Level x where > var :: x -> x -> Tm (Syn a) Inf x > fresh :: String -> (Val x -> x -> t) -> x -> t > base :: x
Cheap hack: don’t name any of your parameters (”", i)! For a more expensive hack, see James’s and my “I am not a number…”.
> instance Level (String, Int) where
> var ("", i) ("", n) = V (n - 1 - i)
> var x _ = X x
> fresh _ f x@("", n) = f (N (X x)) ("", n + 1)
> base = ("", 0)
Let’s make beta normal forms! It’s completely structural, apart from parameters, which get processed as above, and closures, which get reactivated with a fresh variable in the vacant slot.
> betan :: Level x => Tm Sem d x -> x -> Tm (Syn Nrm) d x > betan (c :- vs) = (c :-) < $> traverse betan vs > betan (F (K v)) = (F . K) < $> betan v > betan (F (C (x :. t) g)) = > fresh x $ \v -> (F . L . (x :.)) < $> betan (wnf t (v : g)) > betan (N t) = N < $> betan t > betan (X x) = var x > betan (t :$ e) = (:$) < $> betan t < *> traverse betan e > betan (o :@ vs) = (o :@) < $> traverse betan vs
Kick it off.
> betaQ :: Level x => Tm Sem d x -> Tm (Syn Nrm) d x > betaQ v = betan v base
A handy test function.
> betaEval :: Level x => Tm (Syn a) d x -> Tm (Syn Nrm) Chk x > betaEval t = betaQ (wnf t [])
Uglyprinting.
> ugly :: (Show (Val x), Show x) => [String] -> Tm k d x -> String
> ugly ix (c :- []) = show c
> ugly ix (c :- (t : ts)) =
> show c ++ "(" ++ ugly ix t ++ (ts >>= ((',':) . ugly ix)) ++ ")"
> ugly ix (F (K t)) = "(\\_ -> " ++ ugly ix t ++ ")"
> ugly ix (F (L (x :. t))) = "(\\" ++ x ++ " -> " ++ ugly (x : ix) t ++ ")"
> ugly ix (F (C (x :. t) g)) =
> "(\\" ++ x ++ " -> " ++ show g ++ ugly (x : ix) t ++")"
> ugly ix (N (V i)) = fiddli [] ix i
> ugly ix (N (X x)) = jiggli ix (show x)
> ugly ix (N t) = "(" ++ ugly ix t ++ ")"
> ugly ix (V i) = fiddli [] ix i
> ugly ix (X x) = jiggli ix (show x)
> ugly ix (t :$ e) = ugly ix t ++ " " ++ uggly ix e
> ugly ix (o :@ (t : ts)) =
> show o ++ "(" ++ ugly ix t ++ (ts >>= ((',':) . ugly ix)) ++ ")"
> ugly ix (s :=: K t) = "(" ++ ugly ix s ++ " =: _ in " ++ ugly ix t ++ ")"
> ugly ix (s :=: L (x :. t)) =
> "(" ++ ugly ix s ++ " =: " ++ x ++ " in " ++ ugly (x : ix) t ++ ")"
> ugly ix (t ::: y) = ugly ix t ++ " : " ++ ugly ix y
> uggly :: (Show (Val x), Show x) => [String] -> Elim (Tm k d x) -> String
> uggly ix (A t) = ugly ix t
> uggly ix HD = "!"
> uggly ix TL = "-"
> fiddli :: [String] -> [String] -> Int -> String
> fiddli _ [] i = "~" ++ show i
> fiddli jx (x : ix) 0 = jiggli jx x
> fiddli jx (x : ix) i = fiddli (x : jx) ix (i - 1)
> jiggli :: [String] -> String -> String
> jiggli jx x = case length (filter (x ==) jx) of
> 0 -> x
> i -> x ++ "^" ++ show i
> instance Show (Tm k d (String,Int)) where
> show = ugly []
8>< -----------------------------------------------------------------------
Here's stuff that 6.12 will just do.
> instance Traversable Elim where
> traverse f (A t) = A < $> f t
> traverse f HD = pure HD
> traverse f TL = pure TL
> instance Functor Elim where
> fmap = fmapDefault
> instance Foldable Elim where
> foldMap = foldMapDefault
Here's a bit of shovelling
> data Sem = PxSem
> data Syn a = PxSyn a
> data Rdu = PxRdu
> data Nrm = PxNrm
> data Inf = PxInf
> data Chk = PxChk
She will find it; she will bind it; she will stick it with glue glue glue.