Haskellで再帰的な構文木にFix(不動点)を導入してみる

2018-03-20 / [haskell] [ghc] [compiler]

まえおき

例によって僕の記事など読まなくても下記のリンクで解説されているので、Haskell楽しいなと思う人はこちらをどうぞ。

An Introduction to Recursion Schemes

生きるのに疲れた人は半分白目のゆるい気持ちで以降を読んでね。

Haskellで抽象構文木 (AST) にメタデータを付与する

以前この記事でASTへのメタデータの埋め込み方について少し整理して、下記のようなアプローチがあることを明らかにした。

メタデータを保存するための値コンストラクタをASTのブランチとして定義する
メタデータを保存するラッパーを定義する

加えて

Fixを使ってなんかファンシーにする

というアプローチについて最後に少し言及した。これについては当時の僕の頭では理解が追いつかなかったが、いま少しだけ近づけてきた気がするのでまたしても整理してみる。

導入

僕達は日常的に再帰的な構文に出くわしている。

ラムダ項の定義とかもうまさしくそれ。

t ::= x λx. t t t

型システム入門のP.40から拝借

Haskellで書くと、例えばこうなる。

type Id = Stringdata Term = Var Id | Abs Id Term | App Term Term deriving (Eq, Show)

問題

素朴に記述したこのAST。使っているうちに構文木そのもののデータだけでなく、メタデータを保存していきたくなる。

メタデータの例

ソースファイル名
ファイル内の位置情報

普通にアプローチするとこのASTの定義を改造してメタデータを埋め込める場所を用意する。

例えばトークンの開始位置と終了位置を含むデータ Region を埋め込む例の場合。

data Term = Var Region Id | Abs Region Id Term | App Region Term Term deriving (Eq, Show)

しかし、これだとASTのデータ型は純粋な構文以外のデータも持つことになってしまう。できればメタデータをASTをに混ぜるのではなく、分離した上で自然に組み合わせたい。

ということでその立役者となる Cofree を目指すことになる。

しかし、そもそも Cofree の下地となっている Fix という構造がよく解らなかったので、この記事ではまず下記のポイントを確認していこうと思う。

Fix とはなにものなのか
Fix を導入するとなにが起こるのか

再帰的な構文の抽象化

data Term = Var Id | Abs Id Term -- 再帰あり| App Term Term -- 再帰ありderiving (Eq, Show)

もう一度構文定義を再掲。 3つ中2つのコンストラクタは再帰的に Term を受け取るようになっている。

たとえば Abs は具体的なデータとして Term を再帰的に内包できる。

この再帰構造はもう一段抽象化できる。型変数を導入することで下記のようになる。

data TermF a = VarF Id | AbsF Id a | AppF a a deriving (Eq, Show)

コンストラクタの中で Term を持っていたところを型変数 a に括りだした形になる。型をみると解るように、carrier typeを持つこのデータ型は Functor になることができる。言語拡張の DeriveFunctor , DeriveTraversable , DeriveFoldable を使うことで、このデータ型はとても多くの性質を獲得できるようになる。

これで具体的な項を作ってみる。

\> let absx = AbsF "x" $ VarF "x" \> :t absx absx :: TermF (TermF a)

\> let absxy = AbsF "x" $ AbsF "y" $ VarF "y" \> :t absxy absxy :: TermF (TermF (TermF a))

こんな感じ。

項がネストする深さに応じて型もネストしている のが解る。 10の深さの項を作ると、

TermF (TermF (TermF (TermF ...)))

とTermFが10個続いていくことになる。でもこれは扱いにくい。 構成するデータに応じて型が変わり過ぎる。

古いバージョンの定義を使って項を構成して見比べてみよう。

\> let absx = Abs "x" $ Var "x" \> :t absx absx :: Term

\> let absxy = Abs "x" $ Abs "y" $ Var "y" \> :t absxy absxy :: Term

型が単純。

型変数を導入する前はどんな構成方法でも項の型は Term だった。しかし型変数を導入したら、構成方法によって型が変わってしまった。

実はこれでは充分ではない。ネストする、つまり再帰する型を一つの型に収束させる必要がある。

イメージ的には、

TermF (TermF a) -\> TermF TermF (TermF (TermF a)) -\> TermF

のようにネストした型を TermF みたいな何か単純な表現に収束してくれるものを求めている。

Fix

ここで奇妙なデータ型を導入する。

newtype Fix f = In (f (Fix f))

定義方法はこちらに従った: Understanding F-Algebras

複雑な型を内部にもっており、僕も最初に見た時は面食らった。

この Fix を使うと先ほどの再帰的にネストしていく型を収束できる。ただしデータの構成時にちょっとおまけが必要。

\> let absxfix = In $ AbsF "x" $ In $ VarF "x" \> :t absxfix absxfix :: Fix TermF

お、型のネストが消えた。読みやすさのために括弧を使ってみる。

\> let absxfix = In ( AbsF "x" ( In ( VarF "x" ) ) ) \> :t absxfix absxfix :: Fix TermF

TermF を構成したら必ず In でラップしてやるのがミソ。
すると Fix TermF という型が表れて再帰を隠してくれる。もう少し深い項を構成してみよう。

\> let absxyfix = In $ AbsF "x" $ In $ AbsF "y" $ In $ VarF "y" \> :t absxyfix absxyfix :: Fix TermF

やっぱり Fix TermF に収束した。

収束の過程・仕組み

単純に型合わせの過程を観察して、確かに Fix TermF になることを見てみよう。

と言いつつ気力が湧いてきたら書く (ごめんなさい)

Fixは型レベルのfixだった

Fix はデータ型だけどこれと同じような定義を持つ関数がある。

Control.Monad.Fix.fix

型はこんな感じ。

\> :t fix fix :: (a -\> a) -\> a

関数を渡すと値が出てくる変なヤツ。

一方でFixの種 (kind) はどうだろうか？

\> :k Fix Fix :: (\* -\> \*) -\> \*

似すぎ。

もしやと思ってそれぞれの定義を見比べる。

まずfixの定義。 ( こちらを参照 )

fix :: (a -\> a) -\> a fix f = f (fix f)

再帰的に呼び出す fix f の結果に f を適用している。

newtype Fix f = In (f (Fix f))

再帰的に呼び出す Fix f の結果に f を適用している。

一緒じゃん。

形が似ていることは解った。fix を既に知っている人にとっては Fix の振る舞いはもはや疑問の余地がないものだろう。

ただ僕はよく解らないのでちゃんと考える必要がある。

Fixは何なのか

下記のリンクを読めば解る人には解るかもしれない。

HaskellWiki - 不動点と再帰

僕は解らない。

試してみた僕の理解だと Fix f とは

fを再帰的に適用して収束するとこを見つける関数のようなもの

という認識。

Fix f とするとき、 Fix の定義により

Fix f = f(f(f(f(...))))

となる。再帰的に型コンストラクタ f を適用していくことを表現している。

この Fix というデータ型と似た関数版もやはり再帰に関わる。

Control.Monad.Fix.fix

fix f = f(f(f(f(f(...)))))

こうなる。こちらも同様に関数 f を再帰的に適用していくことを表現している。

データ型版も関数版も再帰的に f を再帰的に適用することを表現しているのがポイント。

Fixで得たもの・失ったもの

Fix を使うことで任意の深さで再帰する型 (例えば TermF ) を同一の型で表現することができるようになった。この統一的な表現方式により、冒頭のリンクで言及されているような

再帰的なデータの走査
データ構造の再帰と作用の分離

などを手にすることができる。

この Fix によってもたらされた恩恵の向こうに Cofree が待っているようだ。

得たもの

Cofreeという抽象構造へのステップ。あと少しっぽい。

うまくいけばASTにメタデータを きれいに 載せられるかもしれない！

失ったもの

単純に項を構成する方法。 Fix導入前は項を構成して比較することも容易だった。

\> ( Abs "x" ( Var "x" ) ) == ( Abs "x" ( Var "x" ) ) True

なのでテストを書くのが楽だった。

ところが今回は Fix で構文データをラップする必要が出てくる。

しかしFixという構造自体はEqのインスタンスにできなさそう。同値という性質を定義できない。なのでFixを使って作られた項は単純な比較ができなくなる。

2019-03-03

コメントにて Fix の同値性は定義できる旨をアドバイス頂いたので検証。ご指摘の通り Fix の導入にあたり前述のようなデメリットは無いと分った。

import Data.Functor.Classes (Eq1, eq1)instance Eq1 TermF where liftEq \_ (VarF i) (VarF j) = i == j liftEq f (AbsF i x) (AbsF j y) = i == j && f x y liftEq f (AppF a b) (AppF c d) = f a c && f b d liftEq \_ \_ \_ = Falseinstance (Eq1 f) =\> Eq (Fix f) where (In x) == (In y) = eq1 x y

上記のように2つの定義、すなわち 1. TermF に Eq12. Fix f に Eqを与えることで同値性のテストもできるようになる。

\*Main Lib Data.Functor.Classes\> lhs = In $ AbsF "x" $ In $ AbsF "y" $ In $ VarF "y" \*Main Lib Data.Functor.Classes\> rhs = In $ AbsF "x" $ In $ AbsF "y" $ In $ VarF "y" \*Main Lib Data.Functor.Classes\> lhs == rhs True

こんな風に Fix で包んだ項も比較できる。

GHC 8.6系から使える QuantifiedConstraints を使ってさらに無駄なく定義できるかは確認中。

Eq (Fix f) を定義するためには Eq f を仮定したい
Eq fを仮定したいところだが f はカインドが * -> * なので Eq (f a) を仮定しようとする (ここが自信ない)
Eq (f a) を仮定することで導入される型変数 a が、定義　Eq (Fix f) に現れないためにエラーとなる

* Variable a' occurs more often in the constraint Eq (f a)' than in the instance head Eq (Fix f)' (Use UndecidableInstances to permit this) * In the instance declaration for Eq (Fix f)' | 31 | instance Eq (f a) => Eq (Fix f) where | ^^^^^^^^^^^^^^^^^^^^^^ |

Free f a みたいなデータ型に Eq のインスタンス定義を与えるならいけそう。

FixやCofreeは本当に必要か？

エレガントに見えるけど率直さを失った。本当に必要な抽象か？

比較してみる

1. メタデータを保存するための値コンストラクタをASTのブランチとして定義する

ASTに位置情報という付加情報のためのブランチを作る。簡単、率直だが美しくはない。

ASTの規模が小さいならブランチを作るコスト、それらを分解するコストは大したことないのでこれでいい。というかSML/NJがこれを導入している実績あるので、同程度の規模ならなんとかなると思っていいんじゃないかな。

人生はエレガンス、がスローガンの人だけ次を読むべき。

2. メタデータを保存するラッパーを定義する

位置情報を保存するラッパーを作る。 ASTそれ自体の定義はピュアに保てる。

今回の Fix も所詮ラッパーなので導入コストについていえば、実は2と変わらなかったりする。その上で構文が Functor や Traversable Foldable を備えるなら応用力では今回の Fix アプローチが勝る。

と、言えなくもない。

ただし、僕はこの Fix ベースの構文定義を使っている実用的なプログラミング言語をまだ目撃していない。事例が無いので何か本質的な瑕疵でもあるのでは、と恐怖している。

誰か Fix 使った構文定義しているプログラミング言語実装の例を知っていたら教えてほしい。

うそ。教えてなくてもいい。 僕が Fix の餌食になるので。

まあ、せっかく学んだのでこのアプローチを簡単に捨てるのはまだ少し惜しい気もしている。ということで、もう少し調査を続行。

次の話題

どうもこの手法、 Recursion Scheme と呼ばれるアプローチらしい。