幻想中的Haskell - Compiling Combinator

【東方】「みこみこ魔理沙」イラスト/相生青唯 [pixiv]

abstract：利用Finally Tagless，我們可以把HOAS的變種編譯上SKI Combinator，同時保留type safety還有extensibility。

前置知識：HOAS

如果你要寫Lambda calculus解釋器，你一定會遇到一個問題：如何表示一個binding?

最簡單的辦法（用string表示variable，substitution就是對所有相等String進行替換）有很大的局限性：

data Expr = Var String | Abs String Expr | App Expr Expr deriving (Show, Eq)nneval :: Expr -> Exprneval (Var n) = Var nneval (Abs n x) = Abs n (eval x)neval (App l@(Var _) r) = App l (eval r)neval (App l@(App _ _) r) = eval (App (eval l) (eval r))neval (App (Abs n l) r) = n eval (subst l) wheren subst (Var n) | n == n = rn subst (Var n) | n /= n = Var nn subst (Abs n x) | n == n = Abs n xn subst (Abs n x) | n /= n = Abs n (subst x)n subst (App ll lr) = App (subst ll) (subst lr)nnterm = Abs "y" (App (Abs "x" (Abs "y" (Var "x"))) (Var "y"))nmain = putStr $ show $ eval termn

在(y (x y x) y)下做替換，就會成為(y y)，改變了語義。

沒有這個問題的替換，叫做capture-avoiding substitution（CAS）。

一個挺不錯的是CAS的做法是，我們可以借用metalanguage的binding來完成這個功能-這叫Higher Order Abstract Syntax

data Expr = Lam (Expr -> Expr) | App Expr Exprn

有了這功能以後，我們不止借去了binding，也借去了語法-我們定義Expr跟定義普通lambda function長得很像，下面就是Y的定義：

y = Lam (f -> let e = Lam (x -> App f (App x x)) in App e e)n

可以看到，我們可以在Lam裡面使用let，而不需要在object language有let。

Evaluator 也一樣可以借過來：

eval (Lam l) = Lam lneval (App (Lam l) r) = eval (l r)neval (App l r) = eval (App (eval l) r)n

有了上面這幾行代碼，我們就『實現』了一個UTLC的解釋器， 跟我念，EDSL（Embedded DSL）大法好（

這問題還有很多奇奇怪怪的做法，比如鴕鳥法（在Simply Typed Lambda Calculus下只要替換的兩邊都是close term就不需要管），有興趣的可以看Bound - School of Haskell

問題：如果你用了HOAS，你就無法對你的Expression做很多操作，比如PrettyPrint/Optimization/Serialization - 你甚至不能把Expression reduce到normal form，因為HOAS不是first order的：你無法「看進」一個函數。我們能不能保留HOAS的易用性的同時支持這些操作？

前置知識：Finally Tagless

我們現在先把Lambda Calculus放一邊，看另一個問題：

data Arith = Lit Int | Plus Arith Arithnneval (Lit i) = ineval (Plus l r) = eval l + eval rn

我們可以很簡單的為Arith增加一個函數（比如pretty printing），但是我們不能為Arith增加一個Constructor（比如Minus），同時保持extensibility跟type safety-如果你增加了一個Constructor，以前的對Arith進行pattern matching的代碼就不是exhaustive的了-在這，就是你eval並沒有處理Minus的情況

在Java中，這個問題就剛好反過來，我們可以增加constructor，但是不能增加函數（比如現在你就不能加入pretty print了）

abstract class Arith {ntabstract int eval();n}nnclass Lit extends Arith {ntint i;ntLit(int i) {nttthis.i = i;nt}ntint eval() {nttreturn i;nt}n}nnclass Plus extends Arith {ntArith l, r;ntPlus(Arith l, Arith r) {nttthis.l = l;nttthis.r = r;nt}ntint eval() {nttreturn l.eval() + r.eval();nt}n}n

這叫做Expression Problem。

這個問題的一種解法，叫Finally Tagless：我們把Arith的每個Constructor表示成函數，但是abstract掉這些函數的返回類型

class Arith repr wheren lit :: Int -> reprn plus :: repr -> repr -> reprnninstance Arith Int wheren lit i = in plus l r = l + rnnexample :: Arith repr => reprnexample = plus (lit 12) (lit 450)n

我們現在可以在兩邊擴展了。

class Minus repr wheren minus :: repr -> repr -> reprnninstance Arith String wheren lit = shown plus l r = "(" ++ l ++ " + " ++ r ++ ")"nninstance Minus Int wheren minus l r = l - rnninstance Minus String wheren minus l r = "(" ++ l ++ " - " ++ r ++ ")"nnexample :: Arith repr => Minus repr => reprnexample = plus (lit 12) (minus (lit 45) (lit 0))nnmain :: IO ()nmain = putStrLn examplen

輸出(12 + (45 - 0))，很好。

看到這，細心的朋友可能會有一個問題：如果我想在Arith這語言裡面加入double（同時保留type safety跟extensibility）怎麼辦？

最簡單的做法是，我們把repr從Type改成Type -> Type。

class Arith repr wheren litI :: Int -> repr Intn plusI :: repr Int -> repr Int -> repr Intn litD :: Double -> repr Doublen plusD :: repr Double -> repr Double -> repr Doublen

回到問題上:

問題：如果你用了HOAS，你就無法對你的Expression做很多操作，比如PrettyPrint/Optimization/Serialization - 你甚至不能把Expression reduce到normal form，因為HOAS不是first order的：你無法「看進」一個函數。我們能不能保留HOAS的易用性的同時支持這些操作？n

我們有一個typeclass：

class Language repr wheren app :: repr (a -> b) -> repr a -> repr bn ??? --we might need more methodn

我們需要一個函數，lam：

Language repr => (repr a -> repr b) -> repr (a -> b)n

而其中，Language中沒有接受函數的Constructor。或者說，我們可以實現Instance Language PrettyPrint。

很明顯，這不可行 - 我們沒有任何辦法獲得一個repr (a -> b)。如果要一個證明，可以看Theorems for Free!

所以我們需要在一定程度上改變類型簽名。

在考慮該如何更改的時候，我們先做出另一個observation：不止我們沒辦法生成repr (a -> b)，因為我們沒辦法生成repr a，我們沒辦法使用(repr a -> repr b)！再說，就算我們可以使用，repr b的類型也跟repr (a -> b)的類型不一樣！

我們再對類型觀察一下，發現另一件事情：由於用戶需要的就是一個repr (a -> b)，所以這個類型不能改。

把三個條件組合在一起，可以推出，我們需要把簽名改成(unknown a -> unknown b) -> repr (a -> b)。而其中我們可以生成unknown a, 並且unknown b可以轉換為repr (a -> b)。

在這之下，unknown的類型呼之若出：unknown x = repr (a -> x)。

我們可以生成一個unknown a - 因為這是repr (a -> a)，identity。

我們也可以從unknown b生成repr (a -> b) - 因為兩者相等。

newtype Next repr a b = Next { unNext :: repr (a -> b) }nnlam :: SKI repr => (Next repr a a -> Next repr a b) -> repr (a -> b) nlam f = unNext $ f (Next i)n

現在剩下的問題是，unknown（我們改名做Next，提高可讀性）是不是Language的instance。如果不是，使用Next會跟使用其他Language不一樣，就會大大降低易用性。n

我們現在可以考慮下，Language需要支持什麼操作。也就是，???是什麼

我們可以生成一個unknown a - 因為這是repr (a -> a)，identity。

class Language repr wheren app :: repr (a -> b) -> repr a -> repr bn i :: repr (a -> a)n ???n

然後，我們需要支持conv :: repr a -> Next repr b a（因為用戶需要在lam中用原本的term）

換句話說，我們需要repr a -> repr (b -> a)：這是const。

class Language repr wheren app :: repr (a -> b) -> repr a -> repr bn i :: repr (a -> a)n k :: repr (a -> b -> a)n ???n

現在，我們可以先試下實現Next

instance Language repr => Language (Next repr a) wheren app :: Next repr a (b -> c) -> Next repr a b -> Next repr a cn app = undefinedn i = conv in k = conv knnconv :: Language repr => repr a -> Next repr b anconv x = Next (app k x)n

因為我們需要轉換函數conv，把原本的term變成Next的term，所以就加入了k

現在正好就可以用conv來把原本的基本construct lift到Next裡面去

但是，app無法lift進去：我們要好好考慮怎麼做

如果我們unwrap掉app的類型，我們會得到

repr (a -> b -> c) -> repr (a -> b) -> repr (a -> c)n

如果repr是Eval的話（換句話說(a -> b -> c) -> (a -> b) -> (a -> c)），這可以實現：abc -> ab -> a -> abc a (ab a)。所以我們只需要把這個類型作為基礎method加入language，然後就可以（這個函數在Language內只需要用conv實現）

如果你有好好的學Combinatorial Logic的話，就會一眼認出這是SKI的S。換句話說，Language需要支持S。這樣，整個language就是SKI Combinator（注意：因為是typed的，所以這並不是圖靈完備的。手動加入一個Y就能解決這個情況）

{-# LANGUAGEn MultiParamTypeClasses,n RankNTypes,n ScopedTypeVariables,n FlexibleInstances,n FlexibleContexts,n UndecidableInstances,n IncoherentInstances,n PolyKinds #-}nnclass SKI repr wheren app :: repr (a -> b) -> repr a -> repr bn s :: repr ((a -> b -> c) -> (a -> b) -> a -> c)n k :: repr (a -> b -> a)n i :: repr (a -> a)nnnewtype ShowTerm x = ShowTerm { showTerm :: String }nninstance SKI ShowTerm wheren app f x = ShowTerm $ "(" ++ showTerm f ++ " " ++ showTerm x ++ ")"n s = ShowTerm "S"n k = ShowTerm "K"n i = ShowTerm "I"nnnewtype Next repr a b = Next { unNext :: repr (a -> b) }nnconv :: SKI repr => repr a -> Next repr b anconv = Next . app knninstance SKI repr => SKI (Next repr a) wheren app f x = Next $ app (app s $ unNext f) $ unNext xn s = conv sn k = conv kn i = conv innlam :: SKI repr => (Next repr a a -> Next repr a b) -> repr (a -> b)nlam f = unNext $ f (Next i)nnc :: SKI repr => repr ((a -> b -> c) -> b -> a -> c)nc = lam (abc -> lam (b -> lam (a -> app (app (conv $ conv abc) a) $ conv b)))nnmain :: IO ()nmain = putStrLn $ showTerm cn

我們額外的加入了一個show，來表示這的確是first order的。

代碼過Type Check了。一切都解決了嗎？不！

上述代碼輸出了：

((S ((S (K S)) ((S ((S (K S)) ((S (K K)) (K S)))) ((S ((S (K S)) ((S ((S (K S)) ((S (K K)) (K S)))) ((S ((S (K S)) ((S (K K)) (K K)))) ((S (K K)) I))))) ((S (K K)) (K I)))))) ((S ((S (K S)) ((S (K K)) (K K)))) (K I)))n

這個什麼鬼。。。

被刷屏的原因是，

app f x = Next $ app (app s $ unNext f) $ unNext xn

會把每一個app變成兩個app，成為了指數增長。

解決方案也很簡單：在大部分的時候，一顆AST（HOAS的）的大部分subtree都沒有跟Var有任何聯繫，這時候我們只需要保存原tree，最後k一次就好

data Next repr a b = Fast (repr b) | Slow (repr (a -> b))nnunNext :: SKI repr => Next repr a b -> repr (a -> b)nunNext (Slow x) = xnunNext (Fast x) = app k xnninstance SKI repr => SKI (Next repr a) wheren app (Fast f) (Fast x) = Fast $ app f xn app (Slow f) (Slow x) = Slow $ app (app s f) xn app (Slow f) (Fast x) = app (Slow f) (Slow $ app k x)n app (Fast f) (Slow x) = app (Slow $ app k f) (Slow x)n s = Fast sn k = Fast kn i = Fast innlam :: SKI repr => (Next repr a a -> Next repr a b) -> repr (a -> b)nlam f = unNext $ f (Slow i)n

輸出：

((S ((S (K S)) ((S (K K)) ((S (K S)) ((S ((S (K S)) ((S (K K)) I))) (K I)))))) (K ((S (K K)) I)))n

現在這貨勉強能看，並且如果你用S (K X) Y = compose X Y這條規則簡化下的話，還是知道他是在說什麼的。。。

我們再做點微小的工作吧：需要用戶手動填conv（在優化後叫Fast）實在太不人道了，我們試試看用subtyping自動的做轉換。

class NT l r wheren conv :: l t -> r tnninstance NT l r => NT l (Next r a) wheren conv = Fast . convnninstance NT x x wheren conv = idnnlam :: forall repr a b. SKI repr =>n ((forall k. NT (Next repr a) k => k a) -> (Next repr a) b) -> repr (a -> b)nlam f = unNext $ f (conv (Slow i :: Next repr a a))nnc :: SKI repr => repr ((a -> b -> c) -> b -> a -> c)nc = lam (abc -> lam (b -> lam (a -> app (app abc a) b)))n

我們的唯一改動，就是Next repr a a變成了Next repr a a的所有Supertype-這樣當我們需要『向上轉換』的時候，haskell就會自動完成。

另：NT是Natrual Transformation的簡寫，應該看成subkinding，直接subtype會報錯

這個方法是type safe的（trivial），同時也是可擴展的：我們這就加入Arith，並且加入eval功能

class Arith repr wheren int :: Int -> repr Intn add :: repr (Int -> Int -> Int)nninstance Arith ShowTerm wheren int x = ShowTerm $ show xn add = ShowTerm "add"nnnewtype Eval x = Eval { eval :: x }nninstance SKI Eval wheren app f x = Eval $ eval f $ eval xn s = Eval (abc ab a -> abc a (ab a))n k = Eval constn i = Eval idnninstance Arith Eval wheren int = Evaln add = Eval (+)nninstance Arith repr => Arith (Next repr a) wheren int x = Fast (int x)n add = Fast addnndouble :: SKI repr => Arith repr => repr (Int -> Int)ndouble = lam (i -> app (app add i) i)nnmain :: IO ()nmain = putStrLn $ showTerm doublen

練習：

1. 在HOAS構造出一個在UTLC（Untyped Lambda Calculus）中沒對應的Term
2. c的輸出還可以優化。加入更多的基本combinator，然後縮短c的pretty print的長度
3. 有很多表示LambdaCalculus的方法， SKI只是一種，試下用其他的方法表達
4. Expression Problem也有很多解法，比如Object Algebra，Data Type a la carte，換一種表示法
5. 用自己喜歡的語言重寫上面的代碼，看看那個語言更好（劃掉）

另外：

感謝@王瑞康 ，最終版lam是他寫的，當初腦抽了，一定要肝minimal type，肝了兩天，然而Haskell不認QAQ

GitHub - MarisaKirisame/CompilingCombinator: Code for my blog這是代碼

推薦閱讀：