System F をHaskellとPythonで実装した
無事夏休みに突入して時間ができたので再びTaPLを読み始めました．半年触っていなくても進行，保存の証明が書けるあたり，春の自分はずいぶんしっかりと勉強していたようです．春は22章の型再構築まで読んでいたので，ひとまず23章のSystem Fから読んでサクッと実装しました．Pythonが書きたかったので，パーサーだけHaskellで書いてそれ以外をPythonで書くというよく分からない構成で実装していますが，いろいろと学びがあったのでそれを記していきます．
System Fとは
変数，抽象，適用からなる単純型付きラムダ計算に型抽象と型適用を加えて拡張した計算体型のことを指します．パラメータ化した型による計算ができることから多相ラムダ計算とも呼ばれます．この体型のみでは基本型が存在せず型の具体化が十分にできないので，Bool型の構文を追加してそれらしい操作ができるようにしています．単純型付きラムダ計算と同様に進行，保存は成り立ちますが，型注釈を全て取り去った項に対応する正しく型付けされた項が存在するかという問題（いわゆる型再構築問題）は決定不能となります．
以下に多相恒等関数の例を示します．
実装方針
基本はPythonで書きましたが，Pythonのパーサーが体に悪いということを聞いていたので構文解析部分だけHaskellで書きました．HaskellとPythonの仲介はJSONで行っています．stackのおかげでHaskellの環境構築のハードルは下がっており，こうしてスクリプト的に使うこともできるようになってきています．
構文
BNFを以下に示します．関数適用と型適用が混ざって連鎖することを許すので多少トリッキーな構文になっています．
<termBody>
:= <lambdaAbst>
| <typeAbst>
| <generalApp>
<lambdaAbst>
:= "\" <var> <typeAnnotation>opt <termBody>
<typeAnnotation>
:= <typeUnit>
| <typeUnit> "->" <typeAnnotation>
<typeUnit>
:= "Bool"
| <tyVar>
| "(" <tyAnnot> ")"
<termIf>
:= "if" <termBody> "then" <termBody> "else" <termBody>
<typeAbst>
:= "\" <tyVar> <termBody>
<generalApp>
:= <unit> <appChain>
<appChain>
:= "[" <tyAnnot> "]" <appChain>
| <unit> <appChain>
| EOL
<unit>
:= <termIf>
| "true"
| "false"
| <var>
| "(" <termBody> ")"
<var>
:= lower char
<tyVar>
:= upper char
HaskellでJSONを出力する
以下のリンクを参考にしました．
Data.AesonでJSONを扱う | saito's memo
ジェネリクスの仕組みは分かりませんが，ユーザー定義データ型から良しなにインスタンスを導出してくれるので手軽にJSON出力ができます．
PythonでASTを組む
Pythonには代数的データ型やパターンマッチといった再帰的な構造を積極的にサポートする機構が用意されていません．Haskellでは自然に書けていた eval などの関数を書くにも一苦労です．実装に困って @ymyzk 氏に質問したところ，このような場合に有効なVisitorパターンを教えていただきました．Visitorパターンとは，走査される側をAcceptorの派生クラスとして定義しておき，accept関数が走査メソッドを持ったVisitorを受け取って動的に分岐する方法です．説明だけではよく分からないと思うので簡単な実装を以下に示します．
class Node(object): """ASTノードの抽象クラス""" def accept(self, visitor): """accept 側のノードに応じて， visitor 側のメソッドが選択される""" return self._accept(self.__class__, visitor) def _accept(self, klass, visitor): method = getattr(visitor, klass.__name__.lower(), None) return method(self) class TmTrue(Node): pass class Eval(object): def tmtrue(self, node): return node
この実装に基づいて評価の例を示します．
TmTrue().accept(Eval())
-> TmTrue()._accept(TmTrue().__class__, Eval())
# visitor のメソッドから TmTrue.lower() = tmtrue を検索してノードを渡す
-> tmtrue(TmTrue())
-> TmTrue()
このパターンが分かってしまえばあとはやるだけです．参照の共有などに気をつけながら書いてあるとおりに実装します．
REPL で遊んでみる
→ python3 main.py > (\x:Bool->Bool x true) (\x:Bool x) true :: Bool > \X (\x:X x) (\X (\x:X x)) :: forall X.X -> X > (\X (\x:X x)) [Bool] true true :: Bool > (\X (\Y (\x:Y x)) [X->X]) [Bool] (\x:Bool x) (\x:Bool x) :: Bool -> Bool > (\X (\Y (\x:Y x)) [X->X] (\x:X x)) [Bool] (\x:Bool x) :: Bool -> Bool