Compiling from the λ-calculus ==================================== Sending channels through channels is an interesting model, but how many algorithms can we really implement this way? It turns out that the π-calculus can implement any computable function. We'll demonstrate this by writing a compiler from λ-terms to π-terms. Here's a simple, untyped lambda calculus with effects: > data Lam > = Lam :@: Lam > | Var Name > | Abs Name Lam > | Eff (IO ()) Lam We'll use a state monad as a source of fresh names. For simplicity, we assume that the input λ-terms do not use any names beginning with `'_'`. > type M a = State [Name] a > > runM :: M a -> a > runM = flip evalState ['_' : show (x :: Integer) | x <- [1..]] > > fresh :: M Name > fresh = state (\(x:xs) -> (x,xs)) > -- With mtl version 1, use 'State' not 'state' > > withFresh :: (Name -> r) -> M r > withFresh f = f <$> fresh Our compiler will produce π-calculus code which needs to send and receive pairs of values. We can encode a pair as a channel with two values enqueued. `mkInp2` and `mkOut2` construct functions for receiving and sending pairs, respectively. > mkInp2 :: M (Name -> (Name, Name) -> Pi -> Pi) > mkInp2 = withFresh $ \pair from (bind1, bind2) p -> > Inp from pair $ > Inp pair bind1 $ > Inp pair bind2 $ > p > > mkOut2 :: M (Name -> (Name, Name) -> Pi -> Pi) > mkOut2 = withFresh $ \pair dest (from1, from2) p -> > New pair $ > Out pair from1 $ > Out pair from2 $ > Out dest pair $ > p Now we come to the compiler itself. The π-term produced by `compile k e` should evaluate the λ-term `e` and send the result to the "continuation channel" named by `k`. > compile :: Name -> Lam -> M Pi > compile k (Var x) = return (Out k x Nil) > compile k (Eff eff a) = Embed eff <$> compile k a We implement a function as a concurrent process which receives arguments through a channel, and sends back results. ("Lambda as a Service"?) The channel elements are pairs of (function argument, channel where result should be sent). > compile k (Abs x b) = do > inp2 <- mkInp2 > f <- fresh > ret <- fresh > body <- compile ret b > return $ > New f $ > Out k f $ > Rep $ > inp2 f (x, ret) body Note that the compiler allocates a fresh name for `ret` just once, but this name is bound to a different channel by each request. A function application compiles according to the usual call-by-value rule: evaluate the function, evaluate the argument, then apply. Actually, these steps happen in three concurrent processes, but the "apply" process demands the argument value before sending it to the function, so we end up implementing strict semantics. > compile k (f :@: x) = do > out2 <- mkOut2 > [f_cont, f_val, x_cont, x_val] <- replicateM 4 fresh > f_proc <- compile f_cont f > x_proc <- compile x_cont x > let app_proc > = Inp f_cont f_val $ > Inp x_cont x_val $ > out2 f_val (x_val, k) Nil > return $ > New f_cont $ > New x_cont $ > (f_proc :|: x_proc :|: app_proc) At the top level of a program, we still need a continuation channel. But we'll never read from this channel, because we're only running the program for its effects. > lambdaToPi :: Lam -> Pi > lambdaToPi b = runM $ do > k <- fresh > New k <$> compile k b

Testing the compiler ==================== We'll test the compiler by doing some arithmetic on [Church numerals](http://en.wikipedia.org/wiki/Church_encoding#Church_numerals). > -- \m n f -> n (m f) > e_mult :: Lam > e_mult = Abs "m" . Abs "n" . Abs "f" $ > (Var "n" :@: (Var "m" :@: Var "f")) > > -- \f x -> f (f (f (... x))) > e_church :: Int -> Lam > e_church n = Abs "f" . Abs "x" $ > foldr (:@:) (Var "x") (replicate n $ Var "f") > > -- \n -> n (\x -> trace "S" x) (trace "0" n) > e_shownum :: Lam > e_shownum = Abs "n" $ > Var "n" :@: (Abs "x" (Eff (putChar 'S') (Var "x"))) > :@: (Eff (putChar '0') (Var "n")) > > -- compute 2 times 3 > e_test :: Lam > e_test = e_shownum :@: (e_mult :@: e_church 2 :@: e_church 3) And we run it like so: ~~~~ GHCi> run M.empty (lambdaToPi e_test) GHCi> 0SSSSSS ~~~~ The answer of 6 is printed to the terminal, asynchronously, in unary. Notes ===== I thought up this particular scheme for compiling to the π-calculus, but it's probably been documented already. I'm not sure my π-calculus interpreter is correct. In particular, the term `(Rep (x :|: y))` is a [forkbomb](http://en.wikipedia.org/wiki/Fork_bomb), when it should be operationally equivalent to `(Rep x :|: Rep y)`. I don't know if fixing this would be easy or hard. Edward Kmett wrote an [interpreter and pretty-printer](http://www.haskell.org/pipermail/haskell-cafe/2010-June/078750.html) for the π-calculus, in the style of "[Finally Tagless, Partially Evaluated](http://www.cs.rutgers.edu/~ccshan/tagless/jfp.pdf)" [PDF] by Carette, Kiselyov, and Shan.