EDSL相關雜記（2）

類型層面的不動點組合子

首先，我們討論怎樣改造一種最簡單的EDSL AST：單類型（每種eval操作總是返回同一類型），且不涉及多種數據類型的互遞歸。以浮點數算術表達式為例：

data Op = Add | Minus | Mult | Divndata Expr = Lit Double | App Op Expr Exprn

可以認為聲明ADT即對已有類型進行運算，生成新類型。我們需要處理的情況有：

• 積類型（Product Type）：新類型的值同時包含一系列子類型的值
• 和類型（Sum Type）：新類型的值包含一系列子類型其中一種的值
• 遞歸類型（Recursive Type）：新類型的值可能包含自身類型的值

非遞歸的情況下，實現二元或多元的積/和類型輕而易舉，比如可以用Tuple代表積類型，用Either代表二元和類型。怎樣實現遞歸類型？我們先從type-level轉移到term-level，思考類似的問題：lambda calculus不允許為term命名，無法進行自調用，如何實現遞歸函數？答案是使用不動點組合子。

fac :: Int -> Intnfac 0 = 1nfac n = n * fac (n - 1)nn-- now fac has no recursionnfac :: (Int -> Int) -> (Int -> Int)nfac f 0 = 1nfac f n = n * f (n - 1)nn-- thanks to lazy evaluationnfix :: (a -> a) -> anfix f = f (fix f)nn-- works like facnfac :: Int -> Intnfac = fix facn

（不妨在草稿紙上手動規約一下fac 3，觀察fix是如何工作的）

在類型層面，我們可以做類似的事情：

data ExprF e = LitF Double | AppF Op e enn-- now we can tell expression tree height through typenne0 :: ExprF ene0 = LitF 233nne1 :: ExprF (ExprF e)ne1 = AppF Add e0 e0nne2 :: ExprF (ExprF (ExprF e))ne2 = AppF Div e1 e1nn-- .. and so on.nnnewtype Fix f = Fix { unFix :: f (Fix f) }nntype Expr = Fix ExprFnn-- now weve recovered our recursive typen

現在，我們將Expr的「遞歸」語義抽離，變成ExprF，然後通過運用類型層面的不動點組合子應用到ExprF上，恢復了遞歸類型。我們首先考慮新的Expr定義如何使用：怎樣寫構造器和解釋器。

lit :: Double -> Exprnlit = Fix . LitFnnapp :: Op -> Expr -> Expr -> Exprnapp op e0 e1 = Fix $ AppF op e0 e1nnevalOp :: Op -> (Double -> Double -> Double)n-- definition omittednnevalExpr :: Expr -> DoublenevalExpr (Fix (LitF x)) = xnevalExpr (Fix (AppF op e0 e1)) = evalOp op (evalExpr e0) (evalExpr e1)n

看上去，除了多了一些語法噪音以外，構造器與解釋器的實現與原來的Expr別無二致。這些額外的麻煩有何意義，與Expression Problem有何聯繫，很快就會揭曉。因為即將使用一系列高級的GHC擴展，我們需要一點準備工作：

{-# LANGUAGE ConstraintKinds #-}n{-# LANGUAGE DataKinds #-}n{-# LANGUAGE DeriveTraversable #-}n{-# LANGUAGE FlexibleContexts #-}n{-# LANGUAGE FlexibleInstances #-}n{-# LANGUAGE GADTs #-}n{-# LANGUAGE KindSignatures #-}n{-# LANGUAGE MagicHash #-}n{-# LANGUAGE MultiParamTypeClasses #-}n{-# LANGUAGE NegativeLiterals #-}n{-# LANGUAGE PolyKinds #-}n{-# LANGUAGE ScopedTypeVariables #-}n{-# LANGUAGE StandaloneDeriving #-}n{-# LANGUAGE TypeFamilies #-}n{-# LANGUAGE TypeOperators #-}n{-# LANGUAGE UndecidableInstances #-}nnimport Control.Monadnimport Data.Functornimport GHC.Extsn

可組合的函子

注意到一個關鍵的事實：ExprF是一個函子（Functor）！藉助DeriveFunctor擴展，可以自動為ExprF生成Functor類實例。函子的一個好特性是可組合：一系列的函子可以組成函子的積/和類型，結果仍然是一個函子，可以實現fmap操作。並非所有代數結構都有這一好特性，比如單子（monad）的和就不一定滿足單子性質。

回到正題。我們的ExprF可以拆解成兩個不同函子的和：

newtype LitF e = LitF Doublen deriving (Functor, Foldable, Traversable)nndata AppF e = AppF Op e en deriving (Functor, Foldable, Traversable)n

現在，我們將LitF、AppF等EDSL的子集稱為signature，每個signature的kind為* -> *，包含的這個類型標籤e我們稱之為hole。使用Data types à la carte實現EDSL的好處，就是在EDSL上的特定操作可分散給不同的signature在不同模塊里加以實現。那麼signature怎樣組合成和類型，這種和類型怎樣構造和解釋？

原始文獻里，函子的和/積類型均實現為二元操作，對多元組合則通過反覆二元和/積實現，實現簡單，所需GHC擴展也較少，但是有一定的缺點（需要有爭議的OverlappingInstances擴展；二元組合需滿足右結合的順序，等等）。與原始文獻中採用的二元和不同，這裡我們實現一個多元和。前方高能代碼！

data Sum :: [* -> *] -> * -> * wheren Here :: f a -> Sum (f : fs) an There :: Sum fs a -> Sum (f : fs) anntype family AllSatisfy (c :: k -> Constraint) (l :: [k]) :: Constraint wheren AllSatisfy _ [] = ()n AllSatisfy f (l : ls) = (f l, AllSatisfy f ls)nnderiving instance AllSatisfy Functor fs => Functor (Sum fs)nderiving instance AllSatisfy Foldable fs => Foldable (Sum fs)nderiving instance (AllSatisfy Functor fs, AllSatisfy Foldable fs, AllSatisfy Traversable fs) => Traversable (Sum fs)nndata N = Z | S Nnntype family FindElem (l :: [k]) (a :: k) :: N wheren FindElem (x : _) x = Zn FindElem (_ : xs) x = S (FindElem xs x)nnclass HasElem fs f (i :: N) wheren inj :: Proxy# i -> f a -> Sum fs an prj :: Proxy# i -> Sum fs a -> Maybe (f a)nninstance HasElem (f : fs) f Z wheren inj _ = Heren prj _ (Here v) = Just vnninstance HasElem fs f i => HasElem (g : fs) f (S i) wheren inj _ v = There (inj (proxy# :: Proxy# i) v)n prj _ (There _) = Nothingnnclass HasElem fs f wheren inj :: f a -> Sum fs an prj :: Sum fs a -> Maybe (f a)nninstance (HasElem fs f (FindElem fs f)) => HasElem fs f wheren inj = inj (proxy# :: Proxy# (FindElem fs f))n prj = prj (proxy# :: Proxy# (FindElem fs f))nntype f :<: fs = HasElem fs fn

代碼里Sum的實現細節無須理解，我們只需要記住其用法即可：

• Sum [f, g, ..] a是f a, g a, ...等一系列值的nested Either類型，也就是多元的函子和
• 當f, g, ...等均為Functor實例，則Sum [f, g, ..]為Functor實例；Foldable/Traversable亦然
• 當類型構造器f是類型構造器列表fs的成員時，則滿足HasElem fs f，該類型類有inj（inject）、prj（project）方法，分別可以將f a注入到Sum fs a中，或嘗試從Sum fs a中提取f a
• 因為HasElem會頻繁用到，所以實現一個類型別名，f :<: fs即代表HasElem fs f

可組合的構造器

前面，我們定義了浮點數算術運算EDSL的兩個signature，LitF和AppF；我們有了Sum這一工具可用於實現多個函子的和；我們可以用Fix將signature加入遞歸的語義，變為完整的表達式類型。現在，怎樣組合這些工具，實現表達式的構造器？

type Expr fs = Fix (Sum fs)nnlit :: LitF :<: fs => Double -> Expr fsnlit = Fix . inj . LitFnnapp :: AppF :<: fs => Op -> Expr fs -> Expr fs -> Expr fsnapp op e0 e1 = Fix (inj (AppF op e0 e1))nne :: (LitF :<: fs, AppF :<: fs) => Expr fsne = app Add (lit 233) (lit 666)n

我們實現了兩個smart constructor，但它們處理的表達式類型是多態的！我們規定表達式類型Expr有一個類型標籤fs，其kind為[* -> *]，即組成這種表達式的signature列表。現在，lit和app的類型簽名也就很容易懂了：只要表達式包含LitF/AppF的支持，那麼lit/app就能構造出該種表達式，而表達式中可能支持的其他signature我們不關心。下面的e是用lit/app構造出的表達式，由於LitF/lit和AppF/app完全可以分離在兩個模塊里定義，我們終於實現了可組合數據類型的構造！

可組合的解釋器

下面看看怎樣解釋我們的可組合表達式。最粗暴的方法，可以寫一個

evalExpr :: Expr [LitF, AppF] -> Doublen

然後實現過程直接基於遞歸與模式匹配。但我們希望實現可組合的解釋器，比如新增一個signature時，其他signature的解釋器實現不需要動，不需要重編譯。這是辦得到的：

type Alg f a = f a -> annclass Eval f a wheren evalAlg :: Alg f anntype family EvalCap c fs a :: Constraint wheren EvalCap _ [] _ = ()n EvalCap c (x : xs) a = (c x a, EvalCap c xs a)nninstance EvalCap Eval fs a => Eval (Sum fs) a wheren evalAlg (Here v) = evalAlg vn evalAlg (There vs) = evalAlg vsnncata :: Functor f => Alg f a -> Fix f -> ancata f (Fix t) = f (fmap (cata f) t)nninstance Eval LitF Double wheren evalAlg (LitF x) = xnninstance Eval AppF Double wheren evalAlg (AppF op x y) = evalOp op x y wheren evalOp :: Op -> Double -> Double -- omitting implementationnnevalExpr :: (AllSatisfy Functor fs, EvalCap Eval fs a) => Expr fs -> anevalExpr = cata evalAlgnnr :: Doublenr = evalExpr (e :: Expr [LitF, AppF])n

從上到下解讀一下這段代碼的意思：

• 我們定義了一個類型別名Alg f a = f a -> a，Alg是algebra的意思。f代表一個signature，Alg f a是一個代表「摺疊一層」的函數：假如signature的hole類型為a，那麼這個函數將整個signature摺疊為a。
• Eval f a是一個二元關係，代表「存在Alg f a的signature f和目標類型a」。
• 前面我們定義了Sum可以實現一系列signature的和，當f, g, ...等signature都有Eval實例時，Sum [f, g, ...]自動獲得Eval實例。
• 我們定義了一個叫cata的組合子。cata的參數是一個代表「摺疊一層」的algebra和一個用Fix構建起來的遞歸AST，然後將這個algebra遞歸地應用到AST上，自底向上進行摺疊，直到返回a。為了將algebra應用到AST內層的節點，需要signature滿足Functor實例。
• 最終的解釋函數是evalExpr，它處理的AST類型也是多態的：只要signature列表裡每個成員都存在摺疊到a的algebra，並且是Functor實例，那麼evalExpr就能將整個AST摺疊到a。
• 為LitF和AppF定義了「摺疊到Double」的algebra以後，EDSL的解釋器完成了，可以用evalExpr將前面的表達式e計算出結果。這裡手動標了一下類型簽名，因為e和evalExpr都是多態的，不限定e的signature的話，有可能存在額外signature不滿足evalExpr的constraint。

現在，這個解釋器的實現不僅滿足了可組合性的要求，而且揭示了一個源自範疇論的recursion scheme（遞歸設計模式）——catamorphism，通用化的fold操作。

更複雜的解釋器

我們再舉2個更複雜的解釋器例子：一個是EDSL的AST變換，一個是monadic解釋器。

首先講AST變換。我們引入一個新的signature：NegF，代表將某個表達式的值取反。然後我們需要實現一個（可組合的）函數，將含NegF的表達式變換到不含NegF的表達式。

newtype NegF e = NegF en deriving (Functor, Foldable, Traversable)nnneg :: NegF :<: fs => Expr fs -> Expr fsnneg = Fix . inj . NegFnnclass Desugar f fs wheren desugarAlg :: Alg f (Expr fs)nninstance EvalCap Desugar fs gs => Desugar (Sum fs) gs wheren desugarAlg (Here v) = desugarAlg vn desugarAlg (There vs) = desugarAlg vsnninstance LitF :<: fs => Desugar LitF fs wheren desugarAlg = Fix . injnninstance AppF :<: fs => Desugar AppF fs wheren desugarAlg = Fix . injnninstance (LitF :<: fs, AppF :<: fs) => Desugar NegF fs wheren desugarAlg (NegF x) = app Mul x (lit -1)nndesugarExpr :: Expr [LitF, AppF, NegF] -> Expr [LitF, AppF]ndesugarExpr = cata desugarAlgn

這裡，我們定義了Desugar類型類代表去掉NegF的desugar algebra，Desugar f fs代表signature f能夠Desugar到類型標籤為fs的表達式。照例，我們定義了LitF和AppF的Desugar實例（不做任何變換），以及Sum的Desugar實例。對於NegF，我們將其變換為「乘以-1」的表達式。最後，將cata應用到這個desugar algebra，我們得到一個能夠將NegF signature去除的desugar function。

一般而言，基於cata定義可組合解釋器時，如果fold結果類型比較簡單，可以直接復用前面的Eval類型類以及evalExpr；結果類型比較複雜（比如Desugar支持生成多態的新表達式），直接復用Eval或者實現newtype wrapper會比較麻煩，適合的做法就是為每個不同的解釋器定義一個類型類，用於描述不同操作所對應的algebra。

最後，cata操作可以推廣到生成monadic value的cataM，從而便於實現monadic的解釋器處理副作用（I/O、錯誤處理等）：

type AlgM m f a = f a -> m anncataM :: (Traversable f, Monad m) => AlgM m f a -> Fix f -> m ancataM f (Fix t) = join (fmap f (mapM (cataM f) t))nnclass EvalM m f a wheren evalAlgM :: AlgM m f anntype family EvalCapM c m fs a :: Constraint wheren EvalCapM _ _ [] _ = ()n EvalCapM c m (x : xs) a = (c m x a, EvalCapM c m xs a)nninstance EvalCapM EvalM m fs a => EvalM m (Sum fs) a wheren evalAlgM (Here v) = evalAlgM vn evalAlgM (There vs) = evalAlgM vsnninstance EvalM IO LitF Double wheren evalAlgM (LitF x) = putStrLn "Lit" $> xnninstance EvalM IO AppF Double wheren evalAlgM (AppF op x y) = putStrLn "App" $> evalOp op x ynnevalExprM :: (AllSatisfy Functor fs, AllSatisfy Foldable fs, AllSatisfy Traversable fs, EvalCapM EvalM m fs a, Monad m) => Expr fs -> m anevalExprM = cataM evalAlgMnnr :: IO Doublenr = evalExprM (e :: Expr [LitF, AppF])n

總結與課外閱讀

我們初步展現了Data types à la carte：怎樣將EDSL的AST分離成不同的signature，並將其組合起來，實現多態的構造器和基於cata的解釋器。篇幅所限，這裡展示的是最簡單的情況：EDSL是單類型的，不涉及互遞歸，解釋操作上下文不敏感。

進一步了解Data types à la carte，不妨閱讀Wouter Swierstra在JFP上的原文，以及Compositional Data Types。後者進一步解決了context-sensitive、GADT與互遞歸支持，並且實現了除了cata以外的多種其他recursion schemes，對應的compdata庫還帶有一系列Template Haskell函數可以為用戶自定義的signature自動生成smart constructor等boilerplate code。

關於recursion schemes的實現以及更多範疇論與函數式編程的聯繫，可以從recursion-schemes庫，以及大名鼎鼎的Functional programming with bananas, lenses, envelopes and barbed wire一文看起。

下期預告：下一期講Finally Tagless style，作為另一種Expression Problem的解決方案。與本期的狂飆GHC特性相比，finally tagless常常使用普通的Haskell 2010特性即可使用，簡單易懂，之後的文章里用到的頻率也會更高。等到老後面講Freer monad和effect system時，我們將回顧Data types à la carte並揭示它與finally tagless style的奇妙聯繫。

最後一點chit-chat時間：寫專欄真是個不錯的犯拖延症的方法啊。不過接下來一段時間要沉迷學習了，還有幾個黃油待推，距離下次發布得等一段時間咯。。（