EDSL With Typed Lambda Calculus Implemented In Haskell

发表于

EDSL With Typed Lambda Calculus Implemented In Haskell

Abstract

Haskell是一种丰富的语言，它具有各种扩展功能。另外，我们可以将我们定义的语言(比如DSLs)中的lambda表达式embed到或者映射到Haskell中的lambda表达式中，这就是所谓的HOAS(Higher Order Abstract Syntax)。同时我们可以利用FInally Tagless，可以将HOAS表示成SKI Combinator的形式，最后可以添加Y Combinator实现带类型的计算，同时还能拥有很好的extensibility与类型安全。

Binding

Lambda演算虽然非常简单，但是在计算与实现Lambda表达式规约上却有很多方法，主要是在计算策略上的不同，按模型主要分为三类：

  1. Call-by-value:arguments are evaluated before a function is entered
  2. Call-by-name:arguments passed unevaluated
  3. Call-by-need:arguments passed unevaluated but an expression is only evaluated once and shared upon subsequent references

在不同模型下的规约步骤不同:

Call-by-value:

  1. Evaluate x to v
  2. Evaluate f to λy.e
  3. Evaluate [y/v]e

Call-by-name:

  1. Evaluate f to λy.e
  2. Evaluate [y/x]e

Call-by-need:

  1. Allocate a thunk v for x
  2. Evaluate f to λy.e
  3. Evaluate [y/v]e

不管是哪种模型什么策略，都会遇到一个问题，即最后一步做substitution的时候，该如何正确地表示binding。最朴素的想法，substitution就是替换，我们完全可以将后面的expression看做字符串去替换前面变量所有的出现，这样就是一个简单的字符串匹配的问题了，用Haskell强大的模式匹配很快就能解决，代码如下:

data Expr = Var String | Abs String Expr | App Expr Expr deriving (Show, Eq)

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

考虑这样的一个Lambda表达式\y(\x\y x)y

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

运行结果为Abs "y" (Abs "y" (Var "y"))，这样语义就改变了(\x \y x -> \y y变成了与y变量有关的函数)。

所以单纯的字符串替换是不行的，他不能看到一个Lambda表达式中的语义信息所以会出现改变语义的substitution，我们需要需求一种替换，不会出现语义改变的问题，这种替换被称为capture-avoiding substitution（CAS）。

一种主流的方法是将语言embed到另一种metalanguage中，这样我们就借来了metalanguage中的binding，这叫做HOAS。

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

我们定义Expr方式也与定义普通的Lambda function类似，同时对表达式的计算也变得简单了，可以简单地使用Haskell来计算。

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

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

这样的形式目前看来很不错，很好并且很优雅地解决了binding的问题，但是这样的形式是不是完美的呢？很显然存在很多麻烦之处。

首先，我们需要更多时间考虑怎么把一个expression转换成这种的形式，因为我们需要使用Haskell本身的Lambda binder。另外，由于所有的机制都包在Haskell的实现里面，所以即使像PretyPrint/Optimization/writing transformation passes这种简单的操作都会变得异常困难，我们很难看到一个函数本身的结构。所以这种形式只是适合计算的一种很好的形式，并不适合通用的转换。那么我们能不能找到一种方法在保留HOAS优势的同时简单地支持这些操作呢？

Expression problem

首先来看一个expression的问题。这里用经典的“Hutton’s Razor”作为例子，它是使用加法运算+从整数文字建立的简单算术表达式的语言，在Haskell中可以这么表示：

data Exp = Lit Int | Add Exp Exp

这样，比如表达式(1+(2+3))就可以写成：

e1 = Add (Lit 1)
         (Add (Lit 2)
               (Lit 3))

给他写一个eval能够计算形如上面的表达式的值:

eval :: Exp -> Int
eval (Lit n)   = n
eval (Add x y) = eval x + eval y

我们可以很简单的为我们的Exp增加一个函数（比如pretty printing）:

prettyprint :: Exp -> String
prettyprint (Lit n) = show n 
prettyprint (Add x y) = "(" ++ prettyprint x ++ "x" ++
                        prettyprint y ++ ")"

并且不会影响到Exp的extensibility与type safe(我们根本不需要对Exp的constructor进行改变)。但是，当我们试着对我们定义的这个语言表达式做运算符的拓展的时候(比如添加一个乘法运算*)，事情好像就比较麻烦了。首先需要在数据类型Exp中增加一个Mult的constructor，我们还需要在每个涉及到Exp的function中添加case，比如上面的eval与prettyprint。真实世界事件的规模比我们举的这个例子大很多，存在多涉及到类似定义的数据类型的function，作为一个代码的维护者，必须极其小心检查每个function并为每个function加上独特的case——十分煎熬。所以这样的方法不能在为数据类型增加constructor的时候同时保持我们语言的extensibility与type safe。

这是用函数式语言会遇到的问题，我们再尝试用OO的语言实现，看有没有相同的问题。

在Java中定义一个Exp的接口，提供一个抽象方法eval()，上面每个constructor都可以写成继承这个Exp的类，并且实现它的抽象方法:

interface Exp {
    int eval();
}

class Lit implements Exp {
    int n;
    Lit(int n) { this.n = n; }
    int eval() { return n; }
}

class Add implements Exp {
    Exp x, y;
    Add(Exp l, Exp r) { this.x = l; this.y = r; }
    int eval() { return x.eval() + y.eval(); }
}

尝试为其添加一个*运算，会发现简单很多，简单地再继承一下：

class Mult implements Exp {
  Exp x, y;
  Mult(Exp l, Exp r) { this.x = l; this.y = r; }
  int eval() { return x.eval() * y.eval(); }
}

我们不需要碰到其他地方，只用简单地再增加实现一个类就行了。这么看来刚刚函数式语言的问题得到了很好的解决，但是同时带来了新的问题，添加新的方法（比如prettyprint）显得很困难，我们需要对每个class分别实现，即问题完全反过来了。

这种问题被称作expression problem，有一种很直观的解释。

考虑这样的长方形表格，列代表操作，行代表表达式的类型。表格中的元素代表相关类型的相关操作。

Eval
Lit
Add

在函数式语言中，这个表格中元素的定义是以列为单位的。一列所代表的函数表示一个对所有表达式类型的操作。所以在添加一个新的操作(function)的时候即添加新一列的时候很简单。但是在表达式类型即行这个维度上的可扩展性就没这么强了，因为对每列添加一个新行，每个交都是一个新的case，所以很困难。

Eval Prettyprint
Lit
Add
Mult

在面向对象的语言中，表格中元素的定义是由行组织的。每行所代表的表达式类型包含了这个类型下所有的操作(function)。所以对于面向对象语言而言，对于表达式类型的扩展是比较简单的，事实上只要添加一个新的Class。然而添加新的操作即在表格中添加一列比较困难，因为我们要在每个相关的class里面添加这个方法。

于是expression problem呼之欲出：能否在这个表格的横纵两个维度上都保持很好的扩展性同时又不失static guarantees且无需修改已有的代码呢？

Object algebras & finally tagless

Object algebras是一个比较新的用来解决expression problem的OO设计模式。它是在“Extensiblity for the Masses”这篇文章中提出的，之所以收到推崇是因为他用相当简洁优雅的方式解决了expression problem，不需要对现有语言本身做拓展，在主流语言Java或者C#中就能实现。

Object algebras的主要想法与软件工程中的抽象工厂模式很像，即定义一个接口与其中的抽象方法，这样我们就可以用这个工厂来表示表达式，并生产具体的操作工厂。Java代码如下：

interface ExpAlg<T> {
    T lit(int n);
    T add(T x, T y);
}

interface Eval { int eval(); }

class EvalExp implements ExpAlg<Eval> {
    Eval lit(final int n) {
        return new Eval() {
            int eval() {
                return n;
            }
        };
    }
    Eval add(final Eval x, final Eval y) {
         return new Eval() {
             int eval() {
                 return x.eval() + y.eval();
             }
         };
    }
}

这样表达式(1 + (2 + 3)) 可以表示为:

<T> T e1(ExpAlg<T> f) {
    return f.add(
        f.lit(1),
        f.add(
            f.lit(2),
            f.lit(3)));
}

很简单地来计算e1的值:

int v1 = e1(new EvalExp()).eval();

首先来看看怎么在我们的语言中添加新的表达式类型‘乘法’。第一个想到的方法当然是在我们所定义的接口ExpAlg<T>中添加新的方法Mult，那么就回到了我们刚刚遇到的问题。

不改变原有的代码，考虑定义一个新的interface来 extends 我们之前定义的“工厂”：

interface MulAlg<T> extends ExpAlg<T> {
    T mul(T x, T y);
}

同时对这个新的表达式类型的计算该怎么实现呢，也很简单与前面类似extends EvalExp类即可：

class EvalMul extends EvalExp implements MulAlg<Eval> {
    Eval mul(final Eval x, final Eval y) {
        return new Eval() {
            int eval() {
                return x.eval() * y.eval();
            }
        };
    }
}

这样我们做到了在完全不触碰到原有的代码情况下添加了新的表达式类型‘乘法’。

再来看看如何添加新的操作(function)，比如prettyprint。定义一个新的接口，并且实现用它生产具体的工厂：

interface Prettyprint { String prettyprint(); }

class PrettyprintExp implements ExpAlg<Prettyprint> {
    Prettyprint lit(final int n) {
        return new Prettyprint() {
            String Prettyprint() {
                return Integer.toString(n);
            }
        };
    }
    ...
}
class PrettyprintMul extends PrettyprintExp implements MulAlg<Prettyprint> {
    Prettyprint mult(final Prettyprint x, final Prettyprint y) {
        return new Prettyprint() {
            String Prettyprint() {
                return "(" + x.Prettyprint() + " * " + y.Prettyprint() + ")";
            }
        };
    }
}

这里抽象工厂接口ExpAlg<T>被称为对象代数接口，实现它的具体工厂称为对象代数。这个方法是受抽象代数的启发，抽象代数中代数结构由签名描述，签名作为一个接口，说明了在代数结构的基础集上定义的操作类型，一个代数提供这些操作的具体定义，类似于实现接口的类。

我们现在把上面的例子从Java代码转成Haskell代码，从而实现finally tagless。这个方法是在“Finally Tagless, Partially Evaluated”这篇文章中提出的。

Java中的interface对应Haskell中的Typeclass,class对应instance：

class ExpAlg t where
    lit :: Int -> t
    add :: t -> t -> t

newtype Eval = Eval { eval :: Int }

instance ExpAlg Eval where
    lit n   = Eval n
    add x y = Eval $ eval x + eval y

现在可以两边扩展了：

instance MulAlg Eval where
    mul x y = Eval $ eval x * eval y

newtype Prettyprint = Prettyprint { prettyprint :: String }

instance ExpAlg Prettyprint where
    lit n   = Prettyprint $ show n
    add x y = Prettyprint $ "(" ++ prettyprint x ++ " + " ++ prettyprint y ++ ")"

instance MulAlg Prettyprint where
    mul x y = View $ "(" ++ prettyprint x ++ " * " ++ prettyprint y ++ ")"

这里的形式已经和“Finally Tagless, Partially Evaluated”中所提出的基本相同了，只不过在Haskell中不需要将MulAlg定义成ExpAlg的subclass，我们可以直接独立的定义这个typeclass：

class MulAlg t where
    mul :: t -> t -> t

这样所有含有乘法类型的表达式的类型值为(ExpAlg t, MulAlg t) => t。我们同样不需要更改已有的代码便能实现两边的扩展。

这里用到的“Hutton’s Razor”的例子所涉及到的都是Int类型，如果我们想在这个语言里面加入double，该如何实现呢？

答案是用Phantom types。我们给ExpAlg一个类型变量这样t从Type变成了Type->Type.

class ExpAlg t where
    litI :: Int -> t Int
    plusI :: t Int -> t Int -> t Int
    litD :: Double -> t Double
    plusD :: t Double -> t Double -> t Double

注意到表达式ExpAlg并没有t这个值，所以我们称其为phantom type，它只是个假变量用来限制表达式的类型。

The very beginning problem

那么我们能不能找到一种方法在保留HOAS优势的同时简单地支持这些操作呢？

现在我们有这样一个typeclass:

class Language t where 
    app :: t (a -> b) -> t a -> t b
    ...(more method)

而且我们需要这样一个函数lam:

lam :: Language t => (t a -> t b) -> t (a -> b)

在language class中并没有接受这个函数的constructor，或许我们可以实现instance Language PrettyPrint？

很明显方法是不可行的，我们没有办法得到一个t (a -> b)这么个东西，Theorems for Free!这篇文章中给了具体的证明。

所以想法变成了能不能改变t这个类型签名，而且我们为了要生成一个t (a->b)给app，所以假设新的类型签名为unknown，则现在lam：

lam :: (unknown a -> unknown b) -> t (a -> b)

而且我们是可以生成unknown a的，通过得到一个unknown b就可以转换为t (a -> b)。

unknown的类型呼之欲出：unknown x = t (a -> x)。

根据自反性，我们很快得到一个unknown a(t (a -> a))。

我们也可以通过一个unknown b生成t (a -> b)（本身即是）。

现在我们可以写出unknown了把它取名为Next：

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

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

再来看看我们需要在我们的Language中添加什么，首先我们需要一个unknown a，即t (a -> a)，返回自身的一个method。同时为了用户能在lam中用到原来的term需要再添加一个conv:: t a -> Next t b a，在Language中添加一个t a -> t (b -> a)。现在看看我们的Language是不是完备了：

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

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

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

理论上来说我们要把原来class中的基本construct lisft到Next里面去，现在i与k都可以实现，但是会发现app无法lift进Next里的。这里unwrap掉app的类型，会得到：

app :: t (a -> b -> c) -> t (a -> b) -> t (a -> c)

如果对组合逻辑熟悉的话，可以发现这其实就是SKI组合子中的S，所以只要把这个类型作为基础method加入我们的Language里，然后用conv实现就可以了。这样我们的Language整个就是SKI Combinator。它对于无类型的Lambda演算来是完备的，如果我们的language是有类型的话，可以手动再加上一个Y Combinator。事实上这并不是minimal的系统，因为I还可以用S、K来表达：SKKx → Kx(Kx) → x

SKI组合子的实现:

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

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

newtype Prettyprint x = Prettyprint { prettyprint :: String }

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

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

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

instance SKI t => SKI (Next t 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 t => (Next t a a -> Next t a b) -> t (a -> b)
lam f = unNext $ f (Slow i)

c :: SKI t => t ((a -> b -> c) -> b -> a -> c)
c = lam (\abc -> lam (\b -> lam (\a -> app (app (Fast $ Fast abc) a) $ Fast b)))

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

输出结果：

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

现在我们再回到“Hutton’s Razor”这个例子并给他加上SKI Combinator：

class ExpAlg t where
    lit :: Int -> t Int
    add :: t (Int -> Int -> Int)

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

newtype Prettyprint n = Prettyprint { prettyprint :: String }

instance ExpAlg Prettyprint where
    lit n   = Prettyprint $ show n
    add = Prettyprint "add"

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

newtype Eval x = Eval { eval :: x }

instance ExpAlg Eval where
    lit n   = Eval n
    add = Eval $ (+)

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

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

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

instance SKI t => SKI (Next t 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

instance ExpAlg t => ExpAlg (Next t a) where
    lit x = Fast (lit x)
    add = Fast add

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

instance NT (Next r a) (Next r a) where
    conv = id

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

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

double :: (SKI r , ExpAlg r )=> r (Int -> Int)
double = lam (\x -> app (app add x) x)

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

double这个函数将输入的数加倍，用我们的language输出为：

((S ((S (K add)) I)) I)

如果我们再加上Y Combinator就可以实现这个表达式的计算：

Fix (((S ((S (K add)) I)) I))

其中eval (Fix f) = (eval f) (eval (Fix f))。

Conclusion

为了实现一个embed domain specified language(EDSL)，我们首先考虑用Haskell这个metalanguage用HOAS来实现lambda表达式的binding。同时为了解决expression problem我们用tagless的方法将lambda表达式用SKI Combinator的方式来表示，让我们能“看进”一个lambda表达式，了解他的结构，实现诸如prettyprint的功能。

这样我们的EDSL拥有了如下的feature：

  1. 支持typed的lambda calculus。
  2. type safe，可以利用Haskell的类型系统。
  3. 有很好的extensibility，方便地添加类型、方法，易于维护。

References

Expression problem

Extensibility for the Masses

Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages

From Object Algebras to Finally Tagless Interpreters

Haskell/GADT

Lambda calculus