Haskell＋タグレスな型付きDSLで楽々！C言語コード生成

関数型プログラミング言語とコード生成

HaskellやOCamlなどはコンパイラなどの言語処理系の実装を得意としている。さすがに日常的にコンパイラを実装している人はそう多くないと思うけど、例えばコード自動生成はすぐ試せる割に効き目が大きく、仕事を効率化する方法としてぜひ試してみたい選択肢だ。

今回は、Haskellの言語内DSLからC言語のコードを生成する方法（の一つ）を簡単に紹介する。 この方法で、Haskell上のEDSLを使って (1) C言語のソースコードを生成でき、 (2) Haskellの式として評価できる。 このように、わざわざパーサを書かなくても、コンビネータを適当に作ればすぐにDSLを作ってしまえるのも、関数型言語の魅力かもしれない。

taglessな方法

ただし、ちょっと他と違う方法を試す。 OlegさんのサイトにTyped Tagless Interpretations という記事があり、そこで紹介されている方法を追いかける。 バリアント型/代数的データ型を使わず(=tagless)に、型付きのDSLのインタプリタを実装しよう、という内容だ。 そもそも、言語を実装するには、抽象構文木を表現するバリアント型を作るのが普通なのだが、この方法ではバリアントのような具体的な中間表現を使わないという点に特徴がある。

このエントリ末尾のコードを見てほしい。 対象言語の抽象構文木が型クラスで表現されており、 GADTやバリアント型を使っていないことに注目。 同様のコードはOCamlでも書ける。 シグネチャで構文を定義し、モジュールで変換方法を、 ファンクタでDSLの項を書くことになる。

特に「型付きの」DSLをGADT抜きで実装できている点が面白い。GADTにより、対象言語の型情報をうまくHaskell （ないしOCaml）の型システムと結びつけて扱うことができ、型安全なインタプリタないしコンパイラを作ることができるが、taglessな方法では中間表現を経由しないためにそもそもGADTが必要ない。

C言語の構文解析ライブラリ language-c-quote

C言語のコード生成にはlanguage-c-quoteというライブラリを使っている (cabal install language-c-quoteでインストールできる)。 以前紹介したLanguage.Cとは別もので、こちらは[cexp| … |] という構文でC言語のコード片を書くことができる QuasiQuotationの機能を備えており、コード生成が多少やりやすくなっている。

議論

中間表現を経由しないのはメリットだと思う。

• 処理速度の向上（？） パターンマッチのオーバーヘッドがない。
  • 中間表現を排した分、空間効率は良いのだろうと思う。
  • しかしHaskellの場合、最適化がないと辞書渡しのオーバーヘッドが別に加わることになる。OCamlも同様。時間効率が具体的にどうなのかよくわからない…
• HOASのexotic termの問題がない。 言語内のbinderの表現に Higher Order Abstract Syntax (HOAS) を使っているが、 型表現がパラメトリックなので、exotic termがそもそも作れないようになっている。

一方デメリットは…あるのかよくわからない。一見、中間表現を排しているので、項の構造を調べるのが困難な気がしないでもないけれど、例えばOlegさんの論文には項の大きさを計る方法が載っていたり、特に難しいことはないような感じもする。

• 部分評価器 (partial evaluator) の例では、インタプリタとコンパイラの結果の両方を保持しているのが非効率といえなくもない、かな…（わからない）

コード

(ワンライナーを駆使しているのは見逃してほしい…)

{-# LANGUAGE QuasiQuotes, UndecidableInstances, GADTs, RankNTypes, TypeSynonymInstances, FlexibleInstances, 
KindSignatures, TypeFamilies, ScopedTypeVariables, MultiParamTypeClasses, FunctionalDependencies, 
NoMonomorphismRestriction #-}

-- requires GHC>7 (Haskell platform of the current version will suffice)
-- cabal install language-c-quote hashtables

import Prelude hiding (sum)
import Data.Maybe
import Control.Monad
import Control.Monad.ST
import qualified Data.HashTable.ST.Basic as HT
import Language.C.Syntax
import Language.C.Syntax as C
import Language.C.Quote.GCC {- quasiquote! -}
import Data.Loc
import Data.Symbol

type D = Double

--------------------
-- our purely-functional DSL
--------------------

-- unary and binary operators in our DSL
data Op1 = Neg deriving Show
data Op2 = Plus | Minus | Mult | Divi deriving Show

-- 'tagless' representation of the language
class Lang (e :: * -> *) (array :: * -> *) | e -> array, array -> e where
  -- | e1 `op` e2
  binOp :: Op2 -> e D -> e D -> e D
  -- | op e1
  unOp :: Op1 -> e D -> e D
  -- | iter from to init body -- evaluate the 'body', and accumulate it for (to-from+1) times
  iter :: e Int -> e Int -> e D -> (e Int -> e D -> e D) -> e D
  -- | constant of type Int
  int :: Integer -> e Int
  -- | constant of type double
  double :: D -> e D
  -- | let-binding in the target language
  let_ :: String -> e a -> (e a -> e b) -> e b
  -- | index-based array access (yet not be implemented) 
  at :: e Int -> e (array x) -> e x

{-
Above tagless representation is much similar to the type declaration in GADT, 
which should be like following:
data Lang t where
  BinOp :: Op2 -> Lang D -> Lang D -> Lang D
  UnOp :: Op1 -> Lang D -> Lang D
  Iter :: Lang Int -> Lang Int -> Lang D -> (Lang Int -> Lang D -> Lang D) -> Lang D
  Int :: Integer -> Lang Int
  Double :: D -> Lang D
  Let :: String -> Lang a -> (Lang a -> Lang b) -> Lang b
  At :: Lang Int -> Lang (Array x) -> Lang x
-}

--------------------
-- SYNOPSIS
--------------------

-- add x for ten times
tenTimes x = 
  iter (int 1) (int 10) (double 0.0) (\_ acc-> binOp Plus acc x)
  -- literally, this can be read as 
  -- 'foldl (+) 0.0 $ take 10 $ repeat x' in Haskell,
  -- or 'double accum=0.0; for(int i=0; i<=10; i++) { accum += x; } return accum;' in C

-- 
ex1 = tenTimes (tenTimes (double 1.0))

-- Try this:

-- Evaluate it in Haskell:
---- runHaskell ex1
---- ===> 100.0

-- Generate C Code:
---- genCCode (tenTimes (tenTimes (double 1.0)))
---- ===> (evaluated into the code below)
{-
{
    double accum0 = 0.0;
    
    for (int i0 = 1; i <= 10; i0++) {
        double accum1 = 0.0;
        
        for (int i1 = 1; i <= 10; i1++) {
            ;
            accum1 = accum1 + 1.0;
        }
        ;
        accum0 = accum0 + accum1;
    }
    accum0;
}
-}

--------------------
-- Lesson 1. Evaluate everything in Haskell
--------------------

newtype H x = H x
liftH f (H x) = H (f x)
liftH2 f (H x) (H y) = H (f x y)

toHBinOp :: Op2 -> H D -> H D -> H D
toHBinOp Plus = liftH2 (+)
toHBinOp Minus = liftH2 (-)
toHBinOp Mult = liftH2 (*)
toHBinOp Divi = liftH2 (/)

toHUnOp :: Op1 -> H D -> H D
toHUnOp Neg = liftH pred

instance Lang H [] where
  binOp = toHBinOp
  unOp = toHUnOp
  iter (H from) (H to) (H init) f = 
    if from>to then H (init) 
    else let acc = f (H from) (H init) in iter (H (from+1)) (H to) acc f
  int = H . fromInteger
  double = H
  let_ _ x f = f x
  at = liftH2 (flip (!!))

runHaskell :: H a -> a
runHaskell (H x) = x




--------------------
-- Lesson 2. C code generation
--------------------

-- preparation for embedding typed terms into untyped world
class UntypedLang e where
  binOpU :: Op2 -> e -> e -> e
  unOpU :: Op1 -> e -> e
  iterU :: e -> e -> e -> (e -> e -> e) -> e
  atU :: e -> e -> e
  intU :: Integer -> e
  doubleU :: Double -> e
  letU :: String -> e -> (e -> e) -> e

newtype Untyped t z = U {unU::t}
data Dummy a

instance UntypedLang t => Lang (Untyped t) Dummy where
  binOp op (U e1) (U e2) = U $ binOpU op e1 e2
  unOp op (U e) = U $ unOpU op e
  iter (U e1) (U e2) (U e3) f = U $ iterU e1 e2 e3 (\x y -> unU $ f (U x) (U y))
  at (U e1) (U e2) = U $ atU e1 e2
  int i = U $ intU i
  double d = U $ doubleU d
  let_ s (U e) f = U $ letU s e (\x -> unU $ f (U x))


-- my own Q monad for generating fresh names
newtype Q a = Q (forall s. HT.HashTable s String Int -> ST s a)

instance Monad Q where
  Q f >>= g = Q (\ht -> f ht >>= (\x -> case g x of Q g' -> g' ht))
  return a = Q (\_ -> return a)

runQ :: Q a -> a
runQ (Q m) = runST $ do ht <- HT.new; m ht

newName :: String -> Q String
newName str = Q (\ht -> do
    cnt <- liftM (fromMaybe 0) $ HT.lookup ht str
    HT.insert ht str (cnt+1)
    return $ str ++ show cnt
  )

makeVar :: String -> Exp
makeVar str = Var (Id str noSrcLoc) noSrcLoc



-- mapping operators in our DSL into ones in C
toCBinOp :: Op2 -> BinOp
toCBinOp Plus = C.Add
toCBinOp Minus = C.Sub
toCBinOp Mult = C.Mul
toCBinOp Divi = C.Div

toCUnOp :: Op1 -> UnOp
toCUnOp Neg = C.Negate

-- generate C code!!
instance UntypedLang (Q ([BlockItem],Exp)) where
  -- The pair (stmts, exp) :: ([BlockItem], Exp) is the code that first execute C statements 'stmts' then evaluate 'exp'
  -- Although things are provided as 'UntypedLang', the translation should be type-safe.
  -- since terms are firstly typed using typeful constructor functions of 'Lang', then are embedded into untyped world.
  binOpU op e1 e2 = do (s1,x1) <- e1; (s2,x2) <- e2; return (s1++s2,BinOp (toCBinOp op) x1 x2 noSrcLoc)
  unOpU op e1 = do (s1,x1) <- e1; return (s1,UnOp (toCUnOp op) x1 noSrcLoc)
  iterU from to init body = do
    (sf,f) <- from;
    (st,t) <- to;
    (si,i) <- init;
    cntvar <- newName "i";
    accumvar <- newName "accum";
    let (cntvar_, accumvar_) = (makeVar cntvar, makeVar accumvar)
    (sb,body') <- body (return ([],cntvar_)) (return ([],accumvar_))
    return (sf++st++si++ [
      BlockDecl [cdecl|
        double $id:accumvar = $(i);
      |], BlockStm [cstm|
      for(int $id:cntvar = $(f) ; i <= $(t) ; $(cntvar_)++) {
        $items:sb;
        $accumvar_ = $(body');
      }
      |] ], accumvar_)
  intU i = return ([], [cexp| $int:i |])
  doubleU d = return ([], [cexp| $double:(toRational d) |])
  atU idx_ arr_ = do (sidx,idx) <- idx_; (sarr,arr) <- arr_; return (sidx++sarr, [cexp| $arr[$idx] |])
  letU varname exp_ body_ = do
    var <- newName varname;
    (se,exp) <- exp_;
    let assign = BlockDecl [cdecl| double $id:var = $exp; |]
    (sb,body) <- body_ (return ([],makeVar var));
    return (se++[assign]++sb,body)

genCCode :: Untyped (Q ([BlockItem],Exp)) a -> Stm
genCCode (U expr) = runQ block
  where
    block :: Q Stm
    block = do (items,exp) <- expr; return (Block (items++[BlockStm (Exp (Just exp) noSrcLoc)]) noSrcLoc)

Alloyでλ計算（完全版）

ついに、Alloy を使って完全な λ計算 (β簡約) を表現できた…。（前回 は中途半端だった。）
なかなか面白いのは、Alloy がうまくノードを使って無駄なくβ簡約しているところ（Ω=(λx.xx)(λx.xx) で Ω→Ωなど。後に載せる）。

(8/22)フレーム条件のバグを直した。

悩んだ点：破壊的なβ簡約と共有

今までに考えたλ式の表現では、項に共有が生じ得る。例えば、 let f=λx.x in f f のような項ができる。 一方、β簡約を定義するとき、次のような 破壊的操作 を伴う：

1. 関数呼び出しを関数本体に置き換え
2. 関数本体の仮引数を実引数に置き換え

たとえば、 let f=λx.x in f f → f のように簡約されてほしいのだが、上記の方法だと右手のfも破壊されてしまうので、正しい簡約にならない。

Alloy でグラフのコピーを作るには

共有がある場合にはコピーを作っておくことで、破壊の影響を受けないようにした。 ただし Alloy では、再帰的な関数(fun)や述語(pred)の定義ができないので、グラフをトラバースしてコピーを作るような操作は書けない。どうするか？
ここでAlloyは関係論理をベースにしていることを思い出そう。 t2はt1のコピーである、という関係 copy(t1,t2) を作れば、コピーを得られるはずだ。
具体的には、

sig Term { copy : set Term }

という風にフィールドを宣言すれば、 2項関係を作ったことになるので、あとはファクトで「コピーである」とはどういうことかを書けばいい。
また構文木は簡約により変化してしまうので、「ノードがコピー同士である」というのは状態に依存する一時的な性質だ。そこで

sig Term { copy : set Term -> State }

のようにして、状態が決まるとコピーか否かが決まるようにしておく。 (更に書くと、 copy(t1,t2,s) という述語を、 状態sの一つ前の状態におけるt1のコピーを、状態sのt2とする、という意味になるようファクトを書いた）。

モデル図

例のごとくStateでprojectしている。 copy のエッジを無視すれば、正しいβ簡約ができていることがわかるはず。

let f=λx.xx in f f (いわゆる Ω→Ω )

ノード数に無駄がないことに注目。

let f=λxy.x in f f → λzxy.x

コード

open util/ordering[State] as ord // 簡約を、状態の順序で表現

// 状態
some sig State {}

// λ式 (コピー機能つき)
abstract sig Term {
  // t1 -> t2 -> s2 in copy で，状態s2の直前のs1におけるt1の構造を状態s2のt2にコピー
  // (自分自身を指す場合もある)
  copy : Term set -> State 
}

// 変数ノード
sig Var extends Term {}
// λ抽象ノードと関数適用ノード
abstract sig Term1 extends Term { left : Term lone -> State }
sig Abs extends Term1 { bind : Var }
sig App extends Term1 { right : Term lone -> State }

// 項に循環がない (DAGをつくる)
fact nocycle { all s:State | no t: Term | t in t.^(left.s+right.s)  }
// 自由変数はない/λ式の束縛変数は衝突しない（変数を束縛しているλ抽象はただ1つ）
fact oneparent_var { all v:Var | one v.~bind }
// スコープを守る（λ抽象ノードを経由せず辿り着ける変数は存在しない）
fact nofreevar { all s:State | 
  no v:Var | 
   let abs=v.~bind | // 変数を束縛しているλ抽象
   let path = (Term-abs) <: (left.s+right.s) | // このλ抽象を経由しないすべてのパス
   v in Root.^path  
}

// 根
one sig Root extends Term1 { }
// 根は他のノードの子にならない
fact rootIsRoot { no t:Term | some s:State | Root in t.(left.s+right.s) }

// 述語：根からたどれる
pred reachable(s:State, t:Term) {
  t in Root.*(left.s+right.s)
}


/****
  根からたどれるλ式を作る
****/
// 根からたどれるすべての関数適用は引数をもつ
fact appHasChild { all s:State | all t:App | 
  reachable[s,t] iff
  one l2:Term | t.right.s=l2 } 
// 根からたどれるすべての子持ち項は子をもつ
fact term1HasChild { all s:State | all t:Term1 |
  reachable[s,t] iff
  one l1:Term | t.left.s=l1 }


/****
  コピーの定義
****/
fact factCopy {
  // 状態s1における項tをコピーしたものが状態s2における項cである、とは、
 (all s2:State, t,c : Term | t -> c -> s2 in copy =>
  some s1:ord/prev[s2] | // 直前の状態をs1とする
  // 変数の場合、それを束縛するλ式同士がコピーであればよい
  (t in Var => c in Var and ((t.~bind) -> (c.~bind) -> s2 in copy))  and
  // その他の場合、ノード種が同じ、かつ子要素同士がコピーであればよい
  (t in Abs => 
   c in Abs and
   some l1:t.left.s1, l2:c.left.s2 | (l1 -> l2 -> s2) in copy) and
  (t in App => 
   c in App and
   some l1:t.left.s1, l2:c.left.s2 | (l1 -> l2 -> s2) in copy and
   some r1:t.right.s1, r2:c.right.s2 | (r1 -> r2 -> s2) in copy)) and
 // 根のコピーはない
 all s2:State | Root.copy.s2 = none 
}


/****
  動作意味の定義
****/
// 置換
pred replace[s1,s2:State, x:Term, v:Term] {
    all parent : x.~(left.s1+right.s1) | // その変数の親を全てもってきて
    // 次の状態でvに置換する
    (parent.left.s1=x implies parent.left.s2 = v) and
    (parent.right.s1=x implies parent.right.s2 = v)
}

// s1におけるtのコピーを,s2につくる(tにexceptFor以外の親がある場合のみ)
pred makeCopyIfShared[s1,s2:State, t:Term, exceptFor:Term] {
  all parent : t.~(left.s1+right.s1) - exceptFor |
  one c : t.copy.s2 | 
  (parent.left.s1=t implies parent.left.s2=c) and
  (parent.right.s1=t implies parent.right.s2=c)
}

// parentとtの間のエッジに変化がない
pred notChange[s1,s2:State, parent:Term, t:Term] {
  (parent.left.s1=t => parent.left.s2=t) and
  (parent.right.s1=t => parent.right.s2=t)
}

// β簡約の定義
pred beta[s1,s2:State, a:App] {
    some f : Abs | f=a.left.s1 and // 左手はλ抽象
    // 簡約される関数が複数の親をもっていた場合コピー
    makeCopyIfShared[s1, s2, f, a] and
    //関数適用の親を関数本体に置換
    let body = f.left.s1 | //関数本体
    replace[s1, s2, a, body] and
    // 仮引数を実引数(のコピー)に置換
    some v : a.right.s1 | // 右手(実引数)
    let x = f.bind | // 変数
    some v.copy.s2 and // let f = .. in f f のときに項が破壊されるのでコピーを使う
    replace[s1, s2, x, v.copy.s2] and

    // フレーム条件 (ノードとその親を結ぶエッジに変化はない)
    all t:Term | reachable[s1,t] =>
     // 関数適用(全て関数本体に置換)とλ抽象(共有があれば必ずコピーされる)と
     // 変数ノード(全て実引数に置換)は消えるので除外
     !(t=a or t=f or t=x) => 
     all parent : t.~(left.s1+right.s1) | 
      // 簡約で消えるエッジ (関数適用,実引数)と(λ抽象,関数本体)を除外
      !((t=v and parent=a) or (t=body and parent=f)) => 
      notChange[s1,s2,parent,t]
}

// 必ずどこかでβ簡約する
fact factBeta {
  all s1 : State, s2 : ord/next[s1] {
    // 根からたどれる関数適用を持ってくる
    some t : App | reachable[s1,t] and 
    // tをβ簡約
    beta[s1,s2,t]
  }
}

run {} for 8 but 2 State, 2 App // 速い
//run {} for 10 but 3 State, 2 App
//run {} for 10 but 2 State

//Ω→Ωのような項を発見するのに使う
//fact { let s1 = ord/first[] | let s2 = ord/next[s1] | Root.left.s1 -> Root.left.s2 -> s2 in copy}

/**** 
  初期状態で項の共有を防ぐ場合
****/
// left,rightはAbs,Appについて木をつくる（各ノードの親は高々1つかつ互いに素）
/*fact oneparent { 
  let s=ord/first[] |
  all t:Term1 | lone t.(~(left.s+right.s)) && disj [t.~(left.s), t.~(right.s)] 
}*/

Alloyでλ計算（β簡約）する

フォロー記事あり

前回 (Alloyでλ式をつくる) では、λ式を表現するグラフをAlloyで構築した。
今回は、λ計算の核となるβ簡約の一部をAlloyで記述してみる。

扱えるλ式の制限

面倒だったので、モデルに次の制限を導入した。 このため、正確にはβ簡約とはいいがたい…

• 項の共有がない (λ式は木になっている)
  • β簡約のとき，λ抽象を破壊して関数本体に置き換えるため，共有されると困る．
  • 具体的には let f = λx.x in f (f x) のような場合に、 片方のfが簡約されても他方のノードを残しておかなければいけない
• 変数の共有がない (変数は高々1度しか出現しない)
  • 初期状態においてはこの制限を外せるが、そうすると1回簡約した後に項の共有が生まれる

モデル図

Stateでprojectionしている

λx.(λy.λz.z)x → λx.λz.z

λx.λy.x( (λz.λw.w)(λa.a) ) → λx.λy.x(λw.w)

コード

• λ抽象の関数本体や関数適用の左手をleft, 関数適用の右手をrightとした
• 状態遷移を表現するために util/ordering を使った。 これはよくあるやり方で、知らない人は 抽象によるソフトウェア設計 を買うか、がんばって Formally Introducing Alloy Idioms (PDF) を読むといいです。
• 状態によって構文木が変化するのを表すために、例えば、sig Term1 { left : Term lone -> State } などとしている。
  • こう書くと一見 left は状態を返す関数のように見えるがそうではなく、Term1 * Term * State の3項関係になっている。 lone制約は、状態によっては leftエッジがないことを意図している。
  • 便利なことに、 t.left.s のように書けば、 「状態sにおける tの left側の子」を表すことができる。
  • '.' 演算子が 「結合(join)」であるためにこういうことができる。(t.left) が 2項関係 Term * State を表現するので、さらにStateを左から結合すれば Termが得られる.
• フレーム条件が必要だった。 具体的には、状態遷移の前後で、β簡約された項以外の木構造は変化していない、ということをファクトで記述している。

open util/ordering[State] as ord // 簡約を、状態の順序で表現

// λ項
abstract sig Term {}
// 変数ノード
sig Var extends Term {}
// λ抽象ノードと関数適用ノード
abstract sig Term1 extends Term { left : Term lone -> State }
sig Abs extends Term1 { bind : Var }
sig App extends Term1 { right : Term lone -> State }

// 状態
some sig State {}

// 循環がない
fact nocycle { all s:State | no t: Term | t in t.^(left.s+right.s)  }
// 自由変数はない/λ式の束縛変数は衝突しない（変数を束縛しているλ抽象はただ1つ）
fact oneparent_var { all v:Var | one v.(~bind) }
// スコープを守る（変数ノードの親はλ抽象の子孫ノードのどれか）
fact nofreevar { all s:State | all v:Var | v.(~(left.s)+ (~(right.s))) in (v.(~bind)).*(left.s+right.s)  }

// 根
one sig Root extends Term1 { }
// 根は他のノードの子にならない
fact rootIsRoot { no t:Term | some s:State | Root in t.(left.s+right.s) }

// 述語：根からたどれる
pred reachable(s:State, t:Term) {
  t in Root.*(left.s+right.s)
}

run {} for 10 but 2 State

/****
  グラフを作る
****/
// 根からたどれるすべての関数適用は引数をもつ
fact appHasChild { all s:State | all t:App | 
  reachable[s,t] iff
  one l2:Term | t.right.s=l2 } 
// 根からたどれるすべての子持ち項は子をもつ
fact term1HasChild { all s:State | all t:Term1 |
  reachable[s,t] iff
  one l1:Term | t.left.s=l1 }


/**** 
  苦肉の策：共有を防ぐ
****/
// left,rightは木をつくる（各ノードの親は高々1つかつ互いに素）←かなり強い制限になる
fact oneparent { 
  all s : State |
  all t:Term | lone t.(~(left.s+right.s)) && disj [t.~(left.s), t.~(right.s)] 
  }



/****
  動作意味の定義
****/
// 置換
pred subst[s1:State, s2:State, x:Var, v:Term, edge:Term->lone Term->State] {
    all varparent : x.~(edge.s1) | // その変数の親を全てもってきて
    varparent.edge.s2 = v // 次の状態でvに置換する
}

// β簡約
//  簡約対象のAppを指すエッジが leftとrightの場合があるため、 edge としてパラメータ化
pred beta[s1:State, s2:State, a:App, edge:Term->lone Term->State] {
    some f : Abs | f=a.left.s1 and // 左手はλ抽象
    some v : a.right.s1 | // 右手
    some parent : a.~(edge.s1) | //親
    let body = f.left.s1 | //関数本体
    let x = f.bind | // 変数
    parent.edge.s2 = body  and //関数適用の親を関数本体に置き換え
    subst[s1,s2,x,v,left] and subst[s1,s2,x,v,right] // 実引数を仮引数に代入
    // フレーム条件 (残りの項の親に変化はない)
    and all t:Term | (t!=a and t!=f and t!=v and t!=x and t!=body) implies 
    (all parent : t.~(left.s1) | parent = t.~(left.s2)) and
    (all parent : t.~(right.s1) | parent = t.~(right.s2))
}


fact factBeta {
  all s1 : State, s2 : ord/next[s1] {
    some t : App | reachable[s1,t] and // 関数適用を持ってくる
    (beta[s1,s2,t,left] or beta[s1,s2,t,right])
  }
}

Alloyでλ式をつくる

Alloyでλ式を作ってみた。 フォロー記事あり
あまり役に立たない気はするけど、関係の逆(~)を取ったり(反射)推移閉包(*,^)を使う良い練習になった。

（バグがみつかり次第、色々修正している。以下のモデル図はソースを修正しながら作っているので、エンバグされて出なくなっているものもあるかもしれない）

追記(8/20)：簡単な説明

sigで構文木のノードを，sigのフィールドで構文木のエッジを表現した． また，束縛変数を示す bind というエッジを付加した．
さらに，ファクトを用いて

• 循環がない
• 変数以外の項は複数の親に共有されない
• α変換不要 (変数名が衝突しない)
• 変数のスコープが正しい (スコープの外から変数を参照できない)

という制約を記述することで，それらしいグラフを得ることができた．

λx.x

(λxy.yx)(λx.x)

(λx.(λy.y)x)

λx.λy.y(xy)

λx.λy.(x(xx))(yy)

ソース

（うまい人はもっとすっきり書くような気がする）

// λ項
abstract sig Term {}
// 変数ノード
sig Var extends Term {}
// λ抽象ノードと関数適用ノード
abstract sig Term1 extends Term { t1 : Term }
sig Abs extends Term1 { bind : Var }
sig App extends Term1 { t2 : Term }

// 循環がない
fact nocycle { no t: Term | t in t.^(t1+t2)  }
// λ抽象・関数適用は木をつくる（λ抽象・関数適用ノードの親は高々1つかつ互いに素）
fact oneparent { all t:Term1 | lone t.(~(t1+t2)) && disj [t.~t1, t.~t2] }
// 自由変数はない/λ式の束縛変数は衝突しない（変数を束縛しているλ抽象はただ1つ）
fact oneparent_var { all v:Var | one v.(~bind) }
// スコープを守る（変数ノードの親はλ抽象の子孫ノードのどれか）
fact nofreevar { all v:Var | v.((~t1)+(~t2)) in (v.(~bind)).*(t1+t2)  }

// 根
one sig Root { root : Term }
fact rooted { all t:Term | t in (Root.root).*(t1+t2) } // すべての項は根からたどれる

run {} for 10

線形型DSL on Haskell (前回参照) の基本的アイデアと難しい点

前回は、線形型をもつ DSL の例として 線形λ計算を挙げ、実装を示した。 これをもっと押し進めれば、ファイルやネットワーク接続などのリソースの「使い方」をより詳しく指定できる DSL をエンコードできるはずだ (きれいに書けるか、使う人が居るかは別問題;p)。
実装の簡単な説明はコメントにもあるけど、今回はより詳しい説明を試みたい。

前回の記事では、線形型を Haskell でシミュレートするために、

newtype LLC ii jj a = LLC (ii -> (jj, a))

という型を作った(上の定義は IO や t を省いてある)。
ii -> (jj, a) という型を見てもらえばわかるように、これは Stateモナドの一種になっている。

線形性と「スロット」

型 ii, jj は、線形性をもつ変数の「スロット」になっており、各スロットの使用回数を制限することで、「ただ一度だけ使われる」という線形性を実現している。
たとえば Stateモナド実行前に

(F Int, (F String, ())) 

の型を持っていた状態で、 ひとつめのスロットを使うと、

(U, (F String, ())

という型に「変化」し、それ以上そのスロットを使うことはできない。このような計算は

(F Int, (F String, ())) -> ((U, (F String, ()), a)

という Stateモナドの型になる。
(前回のエントリの記法を使うと逆順になり

(Nil :> F String :> F Int) -> (Nil :> F String :> U, a)

となるけれど、それはどっちでもいい)

変数とλ抽象のエンコード

この「変化」は var の型にエンコードされている。 変数のエンコーディングは (var x) となっており、 ここで x には、スロットのある特定の位置を指す (型レベル) 自然数が来ることになっている。

var :: (Update ii n U jj, Pickup ii n (F a)) => n -> LLC ii jj a

だいたいこういう型を持っていたと思う。名前からわかるとおり、 Update ii n U jj は スロット ii の n番目の要素を U に置き換えたものを jj とする、という意味だ。
これにより、「変数を一度使ったら スロットの内容が F a から U に置き換わり、二度とその変数を使えない」という制約を実現している。

一方、λ抽象はこんな型になっていた

lam :: Length ii n => (n -> LLC (F a,ii) (U, jj) b) -> LLC ii jj (a -> b)

ここでのポイントは Length ii n (前回のエントリでは List ii n) だ。これは スロット ii の長さが n であることを示している。そして λ抽象の中では (F a,ii) などとスロットの長さが1増えている。つまり、n はλ抽象によって導入された新しいスロットの番号を指している。
ここでスロットの番号は後ろから数えていることに注意してほしい。新しいスロットを前から数えると常にゼロ番目になってしまい、スロットを指すインデックスの役目を果たさないのだ。
（実はこの「より内側のλ抽象で導入した変数により大きな番号を付番する方法」が de Bruijn level であり、その逆が de Bruijn index になっている。）

残る関数適用は簡単で、関数部分で消費されるスロットと引数部分で消費されるスロットを分離しているだけだ。前回の実装ではたまたま関数部分で使った残りを引数部分で使い切る、というような型になっているが、順番は重要でなく、単に分離することを目的としている。

型推論

理屈では上の通りだが、これをうまく型推論させるにはコツがいる。なぜか？例えば

lam (\x -> var x)

のような項を考えてみるとよい。 このλ式は「他のコードの一部分」であるかもしれず、x の de Bruijn indexlevel が静的には完全に決まらない。
たとえば上の式では x の de Bruijn level は 0 だが、 lam (\y -> lam (\x -> app (var x) (var y))) では 外側に もうひとつλがあるため 1 となる。
このようにgroundな(型変数を含まない)型にはできない x の型は S n のような型になる。
この結果、普通に型推論させると var x の型の Update と Pickup の計算が途中で止まってしまう。

この結果どうなるかというと、型エラーが、全体の型が決まるまで見過ごされてしまうといったことが起こる。

これを防ぐため、 Update と Pickup の定義を、「後ろから数える」ようにして、さらに引き算の定義にうまくパターンマッチを使うことで、「長さnのリストの、後ろから数えて(n+1)番目の要素は、最初の要素である」などと推論させて、うまく型推論を進めている。
具体的には、 n-n=0, (n+1)-n=1, (n+2)-n=2 などと 引き算の性質をうまく使って、変数を含む式(型)から変数を除去している。

Coq等で実現するには？

上記のように、型推論でパターンマッチの仕組みを利用しているので、Coqでストレートに実装するのはむずかしい。
何かもっと単純な仕組み - たとえば元のの実装のように de Bruijn index を使うとか - にしないとだめだ。

線形型つきドメイン特化言語 (DSL) を Haskell上に実装する

線形λ計算というのは、「変数をちょうど一度だけ使わなければならない」という線形型をもったλ計算だ。これを Haskell で実装してみた。「ファイルが開かれたら必ず閉じる」という制約のような、線形型 (linear type) が必要な DSL の実装の参考になるかもしれない。
線形λ計算の実装は、既に Olegさんがやっている。それは変数参照をde Bruijn indexを使って書くようになっている。
一方、この実装は、よりHaskellに近い記法で書けるようになっている。

使用例

λ抽象の前に lam, 関数適用の前に app, 変数参照の前に var が必要である以外は Haskell と同じ記法で書ける。

Linear Lambda Calculus の頭文字をとって LLC モナドという名前にしてある。

LLCモナドの型は LLC t ii jj a となっていて、

t

型のタグ。他のLLCと混ざらないようにするため

ii, jj

LLCモナドの事前条件と事後条件。 線形性をエンコードするために使っている.

a

モナドが持っている値。

という役割を果たしている。

また a :-> b は線形な(?) 関数で、引数が一度しか使われないことを表している。

他に、どうしても出てくる変な型クラスが2つある。

HList ii n

型レベルリストiiの長さがn.

Consume ii jj

線形性をエンコードするために使っている。

こんな感じになる。

-- \a -> \b -> a b
t1 = lam (\a -> lam (\b -> app (var a) (var b)))
-- t1 :: (HList ss' n, Consume xs' xs') => LLC t xs' xs' ((a :-> b) :-> (a :-> b))

-- \a -> a+1
t2 = lam (\a -> app (inj1 (+1)) (var a))
-- t2 :: (HList xs' n, Consume xs' xs', Num a) => LLC t xs' xs' (a :-> a)

-- (\a -> a+1) 1
t3 = app t2 (inj0 1)
-- t3 :: (HList kk n, Consume kk kk, Num b) => LLC t kk kk b
--
-- *Main> (run t3 :: IO Int)
-- 2

-- 線形性の違反は GHCの型エラーとして報告される。
-- 例えば 次の例は 変数 b を使っていないので型エラーになる。
--
-- :t lam (\a -> lam (\b -> var a))
-- <interactive>:1:23:
--     Couldn't match type `F a0' with `U'
--     When using functional dependencies to combine
--       UpdateR (xs :> s) (S n) t (xs' :> s),
--         arising from the dependency `xs n t -> xs''
--         in the instance declaration at Linear.hs:83:10
--       UpdateR ((xs' :> F a_e) :> F a0) (S O) U ((xs' :> U) :> U),
--         arising from a use of `var' at <interactive>:1:23-25
--     In the expression: var a
--     In the first argument of `lam', namely `(\ b -> var a)'

-- 次の例は変数 b を2回使っているので型エラー
-- :t lam (\a -> lam (\b -> app (var a) (app (var a) (var b))))
-- <interactive>:1:41:
--     Couldn't match type `U' with `F (a0 :-> a1)'
--     In the first argument of `app', namely `(var a)'
--     In the second argument of `app', namely `(app (var a) (var b))'
--     In the expression: app (var a) (app (var a) (var b))

t4 = lam (\a -> app (io1 putStrLn) (var a))
-- t4 :: (HList xs' n, Consume xs' xs') => LLC t xs' xs' (String :-> ())

ソース

{-# LANGUAGE 
    MultiParamTypeClasses,FunctionalDependencies,FlexibleInstances,FlexibleContexts,
    UndecidableInstances,OverlappingInstances,NoMonomorphismRestriction,Rank2Types,
    TypeOperators,EmptyDataDecls,KindSignatures,TypeFamilies
    #-}

-- * 線形λ計算をHaskellに埋め込んでみた by @keigoi
--
-- 型付きのドメイン特化言語 (DSL) を Haskellに埋め込んでみる例。
-- 
-- プログラミングにおいて、「このファイルハンドルは必ず閉じる」などという制約を
-- 付与したくなることは多い。
-- このような制約は線形型 (linear type) で実現できるが、Haskellには線形型がないので、
-- 普通のphantom typeの方法ではそういうEDSL を Haskellの上に作ることはできない．
--
-- このコードでは、Oleg の Heterogeneous List のテクニックを使って、
-- 線形性をもつ型システムを Haskell 上に実現する方法を示す．
--
-- 埋め込まれるのは線形λ計算といって、全ての変数をちょうど1回だけ使わなければいけない型システムだ。
-- このコードは Oleg Kiselyov の http://okmij.org/ftp/tagless-final/course/LinearLC.hs 
-- を参考にしている．
-- これも線形型の埋め込みを達成している． その方法は de Bruijn indexに基づくもので、
-- 例えば @lam (lam (app (s z) z))@ は @(\x -> \y -> x y)@ のように書く．
--
-- このコードでは HList (http://okmij.org/ftp/Haskell/types.html#HList) を応用して、
-- もうちょっとプログラマーフレンドリーな形で書けるようになる．
-- たとえば, @(\x -> \y -> x y)@ は @lam (\x -> (\y -> app (var x) (var y))@ と書かれ、
-- これは Haskell の記法に近いのでうれしいはずである．
-- 
-- (ghc-7.0.3で確認したが、 悲しいことに ghc-6.8.2 さんはパニックになってしまう。)

-- | 型レベルの 0 
data O = O deriving Show
-- | 型レベル +1. @'S' n@ は @(n+1)@ を表す.
data S n = S n deriving Show

-- | 型レベル引き算。 HListの操作で、リストを後ろから数えるために使う。
class Sub a b c | a b -> c where
  sub :: a -> b -> c
-- 普通に引き算を定義するとこうなるが、そうすると GHCの型推論が途中で止まってしまい
-- @Sub n n m@ みたいなインスタンスが文脈に残ってしまう。 ここで n-n=0 なので m = O と推論されてほしいのに…。
{-
instance Sub n O n where
  sub n _ = n
instance Sub n m x => Sub (S n) (S m) x where
  sub ~(S n) ~(S m) = sub n m
-}
-- 仕方がないので n-n=0, (1+n) - n = 1, .. などと GHCに教えてあげることにする．
instance Sub n n O where sub _ _ = O
instance Sub (S n) n (S O) where sub _ _ = S O
instance Sub (S (S n)) n (S (S O)) where sub _ _ = S (S O)
instance Sub (S (S (S n))) n (S (S (S O))) where sub _ _ = S (S (S O))
-- and so on..


-- | 型レベル snoc (コンス @(:)@ の左右逆). @xs :> x@ は リスト @xs@ のしっぽに @x@ を加えたリストを表す．
data xs :> x = xs :> x
-- | 型レベル空リスト． (@[]@). 
data Nil = Nil


-- | 長さ @n@ の型レベルリスト. HList と違うのは cons でなく snoc を使っていること． 
--   これは見た目の問題であり別に cons でもかまわない．
class HList xs n | xs -> n where
  len :: xs -> n
instance HList xs n => HList (xs :> x) (S n) where
  len ~(xs :> x) = S (len xs)
instance HList Nil O where
  len _ = O


-- | リスト xs の n 番目の要素を s とする． ここで n 番目とは左から右に数えている
class Pickup xs n s | xs n -> s where
  pickup :: xs -> n -> s
instance (HList xs l, Sub l (S n) m, PickupR xs m s)
    => Pickup xs n s where
  pickup xs n = pickupR xs (sub (len xs) (S n))

-- | Pickupの逆順. リスト xs の n 番目の要素を s とする． ここで n 番目とは右から左に数えている
class PickupR xs n s | xs n -> s where
  pickupR :: xs -> n -> s
instance xs ~ (xs':>t) => PickupR xs O t where
  pickupR (_ :> t) _ = t
instance (PickupR xs' n t, xs ~ (xs':>s')) => PickupR xs (S n) t where
  pickupR (xs' :> _) (S n) = pickupR xs' n

-- | リスト xs の n 番目の要素を t に置き換えたものを xs' とする． ここで n 番目とは左から右に数えている
class Update xs n t xs' | xs n t -> xs' where
  update :: xs -> n -> t -> xs'
instance (HList xs l, Sub l (S n) m, UpdateR xs m t xs') 
 => Update xs n t xs' where
  update xs n t = updateR xs (sub (len xs) (S n)) t

-- | Updateの逆順．
class UpdateR xs n t xs' | xs n t -> xs' where
  updateR ::  xs -> n -> t -> xs'
instance UpdateR (xs:>s) O t (xs:>t) where
  updateR (xs:>_) _ t = xs :> t
instance UpdateR xs n t xs' => UpdateR (xs:>s) (S n) t (xs':>s) where
  updateR (xs:>s) (S n) t = updateR xs n t :> s


---- ここから線形型のはなし

-- | まだ使われていない変数
newtype F a = F a
-- | 使用済み
data U = U
-- | 線形な (引数が一度だけ使われる) 関数
newtype a :-> b = Arr { ext :: a -> IO b }


-- | An indexed monad. @ii@ と @jj@ は 計算の直前と直後の 各変数の状態を示している。
--   たとえば @LLC t (xs :> F Int) (xs :> U) a@ は リストの最後にある
--   Int型の変数がただ一度だけ使われることを示している．
--   t はrunが混ざらないようにするためのタグで、よくあることなので気にしない．
newtype LLC t ii jj a = LLC { run' :: ii -> IO (jj,a) }

-- | 自由変数を含まないLLCの項を実行する．
run :: forall a n jj. (forall t. LLC t Nil Nil a) -> IO a
run s = case s of LLC m -> m Nil >>= \(_,a) -> return a

-- | 変数の型。 たとえば lam (\x -> t) の x は Var n型をもつ．この n は型レベル自然数である．
-- 
--   線形ラムダ計算の変数は一度しか使ってはいけないので、
--   変数に直接その型を付けるのではなく、HListに型を格納しておいて、そこを指すインデックスに型を格納する．
--   その変数を一度使ったら HList が書き換えられ、二度と使えないようになる。
--   そのようにして、線形型の型付けを実現している．
newtype Var n = Var n

infixr 6 :->

-- | 元記事の型クラス `HiHo' ． 
--   ラムダ抽象において
class Consume ii jj where
  consume :: ii -> jj
instance Consume Nil Nil where
  consume _ = Nil
instance Consume ii jj => Consume (ii:>F a) (jj:>F a) where
  consume (ii:>i) = consume ii :> i
instance Consume ii jj => Consume (ii:>F a) (jj:>U) where
  consume (ii:>_) = consume ii :> U

-- | ラムダ抽象
lam :: (HList ii n, Consume ii jj) => (Var n -> LLC t (ii:>F a) (jj:>U) b) -> LLC t ii jj (a :-> b)
lam f = LLC (\ii -> return (consume ii, Arr $ \a -> run' (f (Var $ len ii)) (ii:>F a) >>= \(_,b) -> return b))
    
-- | 関数適用
app :: LLC t ii jj (a :-> b) -> LLC t jj kk a -> LLC t ii kk b
app f x = LLC (\ii -> run' f ii >>= (\(jj,Arr f') -> run' x jj >>= \(kk, x') -> f' x' >>= \b -> return (kk, b)))

-- | 変数の使用
var :: (Pickup ii n (F a), Update ii n U jj) => Var n -> LLC t ii jj a
var (Var n) = LLC (\ii -> return (update ii n U, case pickup ii n of F x -> x))

-- | 定数
inj0 :: x -> LLC t ii ii x
inj0 x = LLC (\ii -> return (ii, x))

-- | 関数定数
inj1 :: (x -> y) -> LLC t ii ii (x :-> y)
inj1 f = LLC (\ii -> return (ii, Arr $ \x -> return (f x)))

-- | 副作用が使える関数定数
io1 :: (x -> IO y) -> LLC t ii ii (x :-> y)
io1 f = LLC (\ii -> return (ii, Arr f))


-- * 例

-- \a -> \b -> a b
t1 = lam (\a -> lam (\b -> app (var a) (var b)))
-- t1 :: (HList ii' n, Consume ii' ii') => LLC t ii' ii' ((a :-> b) :-> (a :-> b))

-- \a -> a+1
t2 = lam (\a -> app (inj1 (+1)) (var a))
-- t2 :: (HList ii' n, Consume ii' ii', Num a) => LLC t ii' ii' (a :-> a)

-- (\a -> a+1) 1
t3 = app t2 (inj0 1)
-- t3 :: (HList kk n, Consume kk kk, Num b) => LLC t kk kk b
--
-- *Main> (run t3 :: IO Int)
-- 2


-- 線形性の違反は GHCの型エラーとして報告される。
-- 例えば 次の例は b を使っていないので型エラーになる。
--
-- :t lam (\a -> lam (\b -> var a))
-- <interactive>:1:23:
--     Couldn't match type `F a0' with `U'
--     When using functional dependencies to combine
--       UpdateR (ii :> s) (S n) t (ii' :> s),
--         arising from the dependency `ii n t -> ii''
--         in the instance declaration at Linear.hs:83:10
--       UpdateR ((ii' :> F a_e) :> F a0) (S O) U ((ii' :> U) :> U),
--         arising from a use of `var' at <interactive>:1:23-25
--     In the expression: var a
--     In the first argument of `lam', namely `(\ b -> var a)'

-- 次の例はbを2回使っているので型エラー
-- :t lam (\a -> lam (\b -> app (var a) (app (var a) (var b))))
-- <interactive>:1:41:
--     Couldn't match type `U' with `F (a0 :-> a1)'
--     In the first argument of `app', namely `(var a)'
--     In the second argument of `app', namely `(app (var a) (var b))'
--     In the expression: app (var a) (app (var a) (var b))



t4 = lam (\a -> app (io1 putStrLn) (var a))
-- t4 :: (HList ii' n, Consume ii' ii') => LLC t ii' ii' (String :-> ())

main = run (app t4 (inj0 "Hello, World!!"))  

Coqで分離論理(separation logic)

分離論理は、ヒープ領域に関する論理結合子をもつ論理体系だ。ホーア論理の拡張であり、ヒープを使うプログラムの仕様を書いたり検証したりといったことに使える。
具体的には、 A ∧ B (AかつB) によく似た、 A ** B という論理結合子が追加されている。これは Aで言及しているポインタと、 Bで言及しているポインタが指しているヒープ領域が、分離されている(≒エイリアシングがない)ことをいっている。

Affeldtさんが、Coqで分離論理を書いて、しかもそれを公開してくださっている。

• http://staff.aist.go.jp/reynald.affeldt/seplog/

C言語で書かれたOSのヒープマネージャや、SmartMIPSのアセンブラで書かれた暗号プリミティブの検証をCoqでやっている。

こういったことを自分でも触れるようになりたいので、ICFEM2006のソースを写経していこうと思う (最新のものは何だか大きいので、ヒープマネージャのものを普通に読んでみる)。といっても、coqtopに入力して頭をひねってみるだけだ…。 ただ、ついでにCoqを再復習したり、Ltac の勉強などをしていきたい。

コンパイル

手元の Coq 8.2pl1 で一部をコンパイルできるところまできた。 パッチ

備忘録

inversion_clear

destructと似てる。 /\ や \/ をバラしたり、帰納法を伴わない場合分けに使う

generalize

環境に仮定を追加するのに使ってる…

• util.v は基本的な補題とか
• heap.v は，後で分離論理の定義で使う store (ローカル変数), heap (ヒープ)　の基礎となるmapの定義と、関連する補題など
• bipl.v は、 store の定義、算術式(expr)、ブール式(expr_b)の構文と意味(evalとeval_b)、分離論理の定義(assert)、関連する補題など
• axiomatic.v は、簡単な手続き型言語の構文と操作的意味(exec)、公理的意味(ホーア論理; semax)、ホーア論理の健全性(semax_sound) ←いまここ
• contrib.v
• vc.v weakest precondition の計算。 vc は多分 verification condition の略

言語

略記法(Notation)	Coq項	C言語	意味
x <- e	assign x e	x = e;	ローカル変数xをeに更新
x <-* e	lookup x e	x = *e;	ローカル変数xをポインタeが指す内容で更新
e *<- f	mutation e f	*e = f;	ポインタeが指す内容をfで更新
x <-malloc e	malloc x e	x=malloc(1);*x=e;	ヒープを確保しeで初期化,ローカル変数xに代入
free e	free e	free(e);	ヒープを開放
c ; d	seq c d	c;d;	連接
while b c	while b c	while(b){c}	while文
ifte a thendo x elsedo y	ifte a x y	if(a){x}else{y}	if文
x -.> f	field x f	x[f]??	(x-.>f) *<- e のように使う

論理

略記法	Coq	意味
e1 |-> e2	mapsto e1 e2l	ヒープはe1のアドレスが指す中身はe2
x |--> l	mapstos x l	例：x |--> (e1::e2::nil) で x |-> e1 ** x+1 |-> e2

証明

Decompose_sepcon H h1 h2

destruct の seplog版。 H:(A**B) s h を A s h1 と B s h2 に分け、さらに h=h1+++h2, h1 # h2 (h1とh2は互いに素)を仮定に追加