給 Idris 寫 JS 後端

01-31

（聽說最近寫文章都流行配超大封面……）

在一票 FP 語言裡面，Idris 是最特殊的之一，因為只有極少數語言能誇下海口說「It compiles, it must work!」，Idris 是其中之一。然而雖然 Coq 和 Agda 說這話底氣更足，不過它們特性太偏 PA，做正經開發的話不如 Idris 和 F* 二位兄弟。而在這兩者中只有 Idris 提供了多後端支持以及正經的 FFI。

然而在默認狀況下，Idris 編譯器會使用 C 後端生成 Native binary（我還給它的 RTS 上過代碼……）。然後 EB 寫了一個 JS 後端，只是這個後端寫的實在不敢恭維：它內嵌了一個堆棧式的虛擬機，然後使用 Tracing 的方式解釋位元組碼。雖然和 C 版行為最一致，但性能和「可理解性」方面都遠遠不如其他的 Functional-to-js 編譯器，像下面這段：

module Mainnnrange : Intnrange = 1000nntestProg : Int -> IntntestProg n = loop nnwherentlmt : Intntlmt = min (n + 100) rangenntloop : Int -> Intntloop i = if i >= lmt then i else loop (i + 1)nnmain : IO()nmain = printLn $ testProg 0n

使用官方後端的話 testProg 相關的部分會變成這個德行（Idris 因為是全程序編譯的，所以 JS 裡面還帶有 Prelude 的部分）：

對比下 @張宏波每天廣告的 Bucklescript

// Generated by BUCKLESCRIPT VERSION 1.2.1 , PLEASE EDIT WITH CAREnuse strict;nnvar Pervasives = require("stdlib/pervasives");nnfunction testProg(n) {n var lmt = Pervasives.min(n + 100 | 0, 1000);n var _i = n;n while(true) {n var i = _i;n if (i >= lmt) {n return i;n }n else {n _i = i + 1 | 0;n continue ;n n }n };n}nnvar range = 1000;nnexports.range = range;nexports.testProg = testProg;n

這是何等的差距……

不過好在，Idris 在設計的時候就考慮了對接多種後端，而且也確實有很多人在做後端的工作，那麼，如果官方後端不夠好的話，自己寫一個不就行了么……（當然了，認為官方後端爛的不只我一個，沒有必要真的從頭去寫。）

項目在這：idris-codegen-js，分化自上游的 rbarreiro/idrisjs。idris-codegen-js 的目標就是打造一個高效和易於理解的 JS backend。

Idris 的編譯流程

OK 說正經的吧，Idris 的編譯流程大體如下圖：

作為一個同樣獻祭了無數 PhD 的項目，Idris 最有技術含量的是第一個部分，LoadSource。在這個步驟中，Idris 使用一種類似 Coq 中執行 LTac 的方式將「上位」的 .idr 源碼繁飾（Elaboration）成一個下位的語言 TT，具體過程參閱 EB 的論文 Idris, a General Purpose Dependently Typed Programming Language。（所以如果你關住比較早的話，估計還用過 Idris 的 Elaborator 腳本，那個就是直接操縱 Elaborator 的過程——當然這東西現在換成 Elaborator Reflection 了。）繁飾完成的 TT 會被寫入相應的 .ibc 文件，同時也被 Idris REPL 使用。

而第二個部分，Compile，則是從 TT 開始一步一步地進行一系列語法變換，最終交給 Codegen 生成目標文件。這個步驟是在一個單獨的進程中運行的，程序名 idris-codegen-#.exe，由 Idris 主程序調用，輸入一組 .ibc，輸出一個目標文件。給 Idris 寫後端實際上就是寫一個新的「idris-codegen-#.exe」，放在 idris 主程序相同目錄下，然後就可以用了……

因此，如果你願意的話完全可以想辦法自己讀 .ibc 文件，自己變換自己輸出，可惜 ibc 不僅是二進位文件而且格式也沒文檔，這種想法也就真的是想想而已了。

更加務實的手段是復用 Idris 的架構，也即上圖中的若干框里的表示，這些中間表示位於 IRTS 下的若干模塊中：

TT，這個是類型信息最完整的，但是較為複雜，而且還用了 HOAS 之類的高端特性，拿來做類型檢查很合適，給後端用就未必了。
LDecl，這個是 TT 編譯後的結果，一種類似 UTLC 的語言，但所有的函數調用都只會調用變數，但 Arity 可能不匹配，即可能產生閉包，也可能調用傳入的參數。
DDecl，這個是在 LDecl 的基礎上進行 Defunctinalize，通過顯式構造數據結構消除閉包構造的產物。到了這一步，所有的函數調用不僅只調用頂層聲明，還抱著 Arity 嚴格匹配。
SDecl 則在 DDecl 上進一步簡化，所有的嵌套函數調用都被提出成 let 的形式。
位元組碼，這個沒有在 IRTS.CodegenCommon.CodegenInfo 中直接給出，需要自己生成，官方的 C 後端就使用了位元組碼。

TT、LDecl、DDecl、SDecl 到位元組碼可以看作一個函數式語言一步一步走向機器底層的路程。在 LDecl、DDecl、SDecl、位元組碼這四者中，LDecl 和各種腳本語言的模式最為相似；DDecl 的模型則接近於 C；SDecl 接近一些 SSA IR；位元組碼就不用說了。在寫後端的時候可以使用其中任意一種作為處理。

考慮到現在是 target 到 JavaScript，屬於一個帶有原生閉包支持的腳本語言，因此使用 LDecl 對應的 Lang 層進行最為合適，不過我們會做一些優化，比如 uncurry 幹掉嵌套函數之類。

Lang 層的結構

Lang 層的模塊名是 IRTS.Lang，其核心部分是 LExp 和 LDecl，定義如下：

data LVar = Loc Int | Glob Namen deriving (Show, Eq)nndata LExp = LV LVarn | LApp Bool LExp [LExp] -- True = tail calln | LLazyApp Name [LExp] -- True = tail calln | LLazyExp LExp -- lifted out before compilingn | LForce LExp -- make sure Exp is evalutedn | LLet Name LExp LExp -- name just for pretty printingn | LLam [Name] LExp -- lambda, lifted out before compilingn | LProj LExp Int -- projectionn | LCon (Maybe LVar) -- Location to reallocate, if availablen Int Name [LExp]n | LCase CaseType LExp [LAlt]n | LConst Constn | LForeign FDesc -- Function descriptor (usually name as string)n FDesc -- Return type descriptorn [(FDesc, LExp)] -- first LExp is the FFI type descriptionn | LOp PrimFn [LExp]n | LNothingn | LError Stringn deriving Eqnn-- 中間省略 FFI 和 PrimFn 的部分nndata LAlt e = LConCase Int Name [Name] en | LConstCase Const en | LDefaultCase en deriving (Show, Eq, Functor)nntype LAlt = LAlt LExpnndata LDecl = LFun [LOpt] Name [Name] LExp -- options, name, arg names, defn | LConstructor Name Int Int -- constructor name, tag, arityn deriving (Show, Eq)nntype LDefs = Ctxt LDecln

LExp 大體上就是一個支持閉包的腳本語言的樣子，LDecl 則包含「函數」聲明以及構造器聲明兩類（Name 是 Idris TT 層的類型，表示各種各樣的名稱，十分複雜）。不過你別看 LExp 分支那麼多，實際上在 Lang 層的 Lambda lifting 之後，LLam 不會給你拿到，真正能出現的組合只有以下這麼幾類：

(LV (Glob n))n(LApp tc (LV (Glob n)) args)n(LLazyApp n args)n(LForce e)n(LLet n v sc)n(LCon loc i n args)n(LProj t i)n(LCase up e alts)n(LConst c)n(LForeign t n args)n(LOp f args)nLNothingn(LError e)n

即使配合上 TCO（LApp 第一個欄位就是是否為 tail call），一個 backend 也就大約 1000 行 Haskell 的篇幅，當然如果你把優化全去掉的話會更短，不過生成出來的 JS 會更慢就是了。

去 Curry 化

Idris 和其他一票函數式語言一樣都是默認 Curry 化的，想要消除的話需要記錄頂層聲明的 Arity，然後在編譯 LApp 的時候比對 args 的長度：

如果兩者相等，很好，生成一個簡單的 JS 函數調用，返回即可；
如果聲明的 arity 比傳入的大，那麼就需要刷一個 lambda，同時進行 curry；
如果聲明的 arity 小於傳入的，那麼在「正常」的調用之後，生成一系列的 JS 調用，每次一個參數。

IRTS 從 L 層到 D 層的實現也與之相似。

對象的表示

由於 Idris 大量使用 datatype，對於 LCon 可以做一個有趣的優化：如果某個構造是 0 元的，就不去刷出一個新對象出來，而是直接返回 tag 的數值，減少構造和解構的開銷。

事實上，如果不考慮 LProj 的話，可以再這裡做更多的 specialize，比如把 Idris 的 List 映射到 JS 的數組等等，不過最簡單的 specialize 就是把 Idris 的 Bool 映射成 JS 的 Boolean，實現非常簡單：查詢出 constructor declaration 之後，如果它是 True 或者 False，改掉實現即可。

目前 idris-codegen-js 使用 {type:tag,$1:arg1,$2:arg2,...} 生成 Idris 的對象，以後則會遷移到對每個構造器生成特化的類來實現。

結果

使用現在的 idris-codegen-js 編譯和上文同一段 Idris 結果是這樣：

可以看出幾點：

Idris 的編譯器有內聯的能力，同時會儘力消除重載函數的 dict passing 開銷，這點比 purescript 強太多……
testProg 被內聯了，連定義都不再導出。testProg 里的 loop 被提出同時改成了兩個參數，lmt 也被提出，成為了函數。
常數 range 也被內聯了。
Type term 和 Proof term 都在 LDecl 前消除，成為 null。

對 idris-codegen-js 感興趣的可以去這兒拉源碼編譯、上 PR 等等。JS Binding 可以去上游 rbarreiro/idrisjs 獲取。

感謝 @Canto Ostinato 幫忙配 stack。

圖片來源：《A Functor Fantasy》章節封面

————————————————————————————————————————

附錄：

Purescript 等效代碼

module Main wherenimport Preludenrange = 1000nntestProg n = -- do some workn let lmt = min (n + 100) range n inn let loop i =n if i >= lmt n then in else loop (i + 1) n inn loop nn

Purescript 生成結果

"use strict";nvar Data_Ord = require("../Data.Ord");nvar Data_Semiring = require("../Data.Semiring");nvar Prelude = require("../Prelude");nvar range = 1000;nvar testProg = function (n) {n var lmt = Data_Ord.min(Data_Ord.ordInt)(n + 100 | 0)(range);n var loop = function (__copy_i) {n var i = __copy_i;n var __tco_done = false;n var __tco_result;n var __tco_i;n function __tco_loop(i) {n var $0 = i >= lmt;n if ($0) {n __tco_done = true;n return i;n };n __tco_i = i + 1 | 0;n return;n };n while (!__tco_done) {n __tco_result = __tco_loop(i);n i = __tco_i;n };n return __tco_result;n };n return loop(n);n};nmodule.exports = {n range: range, n testProg: testProgn};n

Elm 等效代碼

range : Intnrange = 1000nntestProg : Int -> IntntestProg n = -- do some workn let lmt = min (n + 100) range inn let loop i =n if i >= lmt then i elsen loop (i + 1) in loop nn

Elm 輸出 JS

var _user$project$Temp1482759649866537$range = 100;nvar _user$project$Temp1482759649866537$testProg = function (n) {ntvar lmt = A2(_elm_lang$core$Basics$min, n + 1000, _user$project$Temp1482759649866537$range);ntvar loop = function (i) {nttloop:nttwhile (true) {ntttif (_elm_lang$core$Native_Utils.cmp(i, lmt) > -1) {nttttreturn i;nttt} else {nttttvar _v0 = i + 1;ntttti = _v0;nttttcontinue loop;nttt}ntt}nt};ntreturn loop(n);n};n