幻想中的Haskell - Compiling Combinator

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)

eval :: Expr -> Expr
eval (Var n) = Var n
eval (Abs n x) = Abs n (eval x)
eval (App l@(Var _) r) = App l (eval r)
eval (App l@(App _ _) r) = eval (App (eval l) (eval r))
eval (App (Abs n l) r) = 
    eval (subst l) where
    subst (Var n') | n == n' = r
    subst (Var n') | n /= n' = Var n'
    subst (Abs n' x) | n == n' = Abs n' x
    subst (Abs n' x) | n /= n' = Abs n' (subst x)
    subst (App ll lr) = App (subst ll) (subst lr)

term = Abs "y" (App (Abs "x" (Abs "y" (Var "x"))) (Var "y"))
main = putStr $ show $ eval term

在(\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 Expr

有了这功能以后，我们不止借去了binding，也借去了语法-我们定义Expr跟定义普通lambda function长得很像，下面就是Y的定义：

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

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

Evaluator 也一样可以借过来：

eval (Lam l) = Lam l
eval (App (Lam l) r) = eval (l r)
eval (App l r) = eval (App (eval l) r)

有了上面这几行代码，我们就‘实现’了一个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 Arith

eval (Lit i) = i
eval (Plus l r) = eval l + eval r

我们可以很简单的为Arith增加一个函数（比如pretty printing），但是我们不能为Arith增加一个Constructor（比如Minus），同时保持extensibility跟type safety-如果你增加了一个Constructor，以前的对Arith进行pattern matching的代码就不是exhaustive的了-在这，就是你eval并没有处理Minus的情况

在Java中，这个问题就刚好反过来，我们可以增加constructor，但是不能增加函数（比如现在你就不能加入pretty print了）

abstract class Arith {
	abstract int eval();
}

class Lit extends Arith {
	int i;
	Lit(int i) {
		this.i = i;
	}
	int eval() {
		return i;
	}
}

class Plus extends Arith {
	Arith l, r;
	Plus(Arith l, Arith r) {
		this.l = l;
		this.r = r;
	}
	int eval() {
		return l.eval() + r.eval();
	}
}

这叫做Expression Problem。

这个问题的一种解法，叫Finally Tagless：我们把Arith的每个Constructor表示成函数，但是abstract掉这些函数的返回类型

class Arith repr where
    lit :: Int -> repr
    plus :: repr -> repr -> repr

instance Arith Int where
    lit i = i
    plus l r = l + r

example :: Arith repr => repr
example = plus (lit 12) (lit 450)

我们现在可以在两边扩展了。

class Minus repr where
    minus :: repr -> repr -> repr

instance Arith String where
    lit = show
    plus l r = "(" ++ l ++ " + " ++ r ++ ")"

instance Minus Int where
    minus l r = l - r

instance Minus String where
    minus l r = "(" ++ l ++ " - " ++ r ++ ")"

example :: Arith repr => Minus repr => repr
example = plus (lit 12) (minus (lit 45) (lit 0))

main :: IO ()
main = putStrLn example

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

看到这，细心的朋友可能会有一个问题：如果我想在Arith这语言里面加入double（同时保留type safety跟extensibility）怎么办？

最简单的做法是，我们把repr从Type改成Type -> Type。

class Arith repr where
    litI :: Int -> repr Int
    plusI :: repr Int -> repr Int -> repr Int
    litD :: Double -> repr Double
    plusD :: repr Double -> repr Double -> repr Double

回到问题上:

问题：如果你用了HOAS，你就无法对你的Expression做很多操作，比如PrettyPrint/Optimization/Serialization - 你甚至不能把Expression reduce到normal form，因为HOAS不是first order的：你无法“看进”一个函数。我们能不能保留HOAS的易用性的同时支持这些操作？

我们有一个typeclass：

class Language repr where
    app :: repr (a -> b) -> repr a -> repr b
    ??? --we might need more method

我们需要一个函数，lam：

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

而其中，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) }

lam :: SKI repr => (Next repr a a -> Next repr a b) -> repr (a -> b) 
lam f = unNext $ f (Next i)

现在剩下的问题是，unknown（我们改名做Next，提高可读性）是不是Language的instance。如果不是，使用Next会跟使用其他Language不一样，就会大大降低易用性。

我们现在可以考虑下，Language需要支持什么操作。也就是，???是什么

我们可以生成一个unknown a - 因为这是repr (a -> a)，identity。

class Language repr where
    app :: repr (a -> b) -> repr a -> repr b
    i :: repr (a -> a)
    ???

然后，我们需要支持conv :: repr a -> Next repr b a（因为用户需要在lam中用原本的term）

换句话说，我们需要repr a -> repr (b -> a)：这是const。

class Language repr where
    app :: repr (a -> b) -> repr a -> repr b
    i :: repr (a -> a)
    k :: repr (a -> b -> a)
    ???

现在，我们可以先试下实现Next

instance Language repr => Language (Next repr a) where
    app :: Next repr a (b -> c) -> Next repr a b -> Next repr a c
    app = undefined
    i = conv i
    k = conv k

conv :: Language repr => repr a -> Next repr b a
conv x = Next (app k x)

因为我们需要转换函数conv，把原本的term变成Next的term，所以就加入了k

现在正好就可以用conv来把原本的基本construct lift到Next里面去

但是，app无法lift进去：我们要好好考虑怎么做

如果我们unwrap掉app的类型，我们会得到

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

如果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就能解决这个情况）

{-# LANGUAGE
    MultiParamTypeClasses,
    RankNTypes,
    ScopedTypeVariables,
    FlexibleInstances,
    FlexibleContexts,
    UndecidableInstances,
    IncoherentInstances,
    PolyKinds #-}

class SKI repr where
    app :: repr (a -> b) -> repr a -> repr b
    s :: repr ((a -> b -> c) -> (a -> b) -> a -> c)
    k :: repr (a -> b -> a)
    i :: repr (a -> a)

newtype ShowTerm x = ShowTerm { showTerm :: String }

instance SKI ShowTerm where
    app f x = ShowTerm $ "(" ++ showTerm f ++ " " ++ showTerm x ++ ")"
    s = ShowTerm "S"
    k = ShowTerm "K"
    i = ShowTerm "I"

newtype Next repr a b = Next { unNext :: repr (a -> b) }

conv :: SKI repr => repr a -> Next repr b a
conv = Next . app k

instance SKI repr => SKI (Next repr a) where
    app f x = Next $ app (app s $ unNext f) $ unNext x
    s = conv s
    k = conv k
    i = conv i

lam :: SKI repr => (Next repr a a -> Next repr a b) -> repr (a -> b)
lam f = unNext $ f (Next i)

c :: SKI repr => repr ((a -> b -> c) -> b -> a -> c)
c = lam (\abc -> lam (\b -> lam (\a -> app (app (conv $ conv abc) a) $ conv b)))

main :: IO ()
main = putStrLn $ showTerm c

我们额外的加入了一个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)))

这个什么鬼。。。

被刷屏的原因是，

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

会把每一个app变成两个app，成为了指数增长。

解决方案也很简单：在大部分的时候，一颗AST（HOAS的）的大部分subtree都没有跟Var有任何联系，这时候我们只需要保存原tree，最后k一次就好

data Next repr a b = Fast (repr b) | Slow (repr (a -> b))

unNext :: SKI repr => Next repr a b -> repr (a -> b)
unNext (Slow x) = x
unNext (Fast x) = app k x

instance SKI repr => SKI (Next repr a) where
    app (Fast f) (Fast x) = Fast $ app f x
    app (Slow f) (Slow x) = Slow $ app (app s f) x
    app (Slow f) (Fast x) = app (Slow f) (Slow $ app k x)
    app (Fast f) (Slow x) = app (Slow $ app k f) (Slow x)
    s = Fast s
    k = Fast k
    i = Fast i

lam :: SKI repr => (Next repr a a -> Next repr a b) -> repr (a -> b)
lam f = unNext $ f (Slow i)

输出：

((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)))

现在这货勉强能看，并且如果你用S (K X) Y = compose X Y这条规则简化下的话，还是知道他是在说什么的。。。

我们再做点微小的工作吧：需要用户手动填conv（在优化后叫Fast）实在太不人道了，我们试试看用subtyping自动的做转换。

class NT l r where
    conv :: l t -> r t

instance NT l r => NT l (Next r a) where
    conv = Fast . conv

instance NT x x where
    conv = id

lam :: forall repr a b. SKI repr =>
 ((forall k. NT (Next repr a) k => k a) -> (Next repr a) b) -> repr (a -> b)
lam f = unNext $ f (conv (Slow i :: Next repr a a))

c :: SKI repr => repr ((a -> b -> c) -> b -> a -> c)
c = lam (\abc -> lam (\b -> lam (\a -> app (app abc a) b)))

我们的唯一改动，就是Next repr a a变成了Next repr a a的所有Supertype-这样当我们需要‘向上转换’的时候，haskell就会自动完成。

另：NT是Natrual Transformation的简写，应该看成subkinding，直接subtype会报错

这个方法是type safe的（trivial），同时也是可扩展的：我们这就加入Arith，并且加入eval功能

class Arith repr where
    int :: Int -> repr Int
    add :: repr (Int -> Int -> Int)

instance Arith ShowTerm where
    int x = ShowTerm $ show x
    add = ShowTerm "add"

newtype Eval x = Eval { eval :: x }

instance SKI Eval where
    app f x = Eval $ eval f $ eval x
    s = Eval (\abc ab a -> abc a (ab a))
    k = Eval const
    i = Eval id

instance Arith Eval where
    int = Eval
    add = Eval (+)

instance Arith repr => Arith (Next repr a) where
    int x = Fast (int x)
    add = Fast add

double :: SKI repr => Arith repr => repr (Int -> Int)
double = lam (\i -> app (app add i) i)

main :: IO ()
main = putStrLn $ showTerm double

练习：

在HOAS构造出一个在UTLC（Untyped Lambda Calculus）中没对应的Term
c的输出还可以优化。加入更多的基本combinator，然后缩短c的pretty print的长度
有很多表示LambdaCalculus的方法， SKI只是一种，试下用其他的方法表达
Expression Problem也有很多解法，比如Object Algebra，Data Type a la carte，换一种表示法
用自己喜欢的语言重写上面的代码，看看那个语言更好（划掉）

另外：

感谢

@王瑞康，最终版lam是他写的，当初脑抽了，一定要肝minimal type，肝了两天，然而Haskell不认QAQ

GitHub - MarisaKirisame/CompilingCombinator: Code for my blog这是代码