GADTを用いた型安全なCPS変換の実装

概要

CPS変換とはラムダ項と継続を入力として型Xを持つラムダ項を出力するプログラム変換である。
HaskellのGADTという機能を使うと型Tを持つラムダ項を表すデータ型Term Tを定義できる。
CPS変換が正しいことは
cps :: Term T -> Term ([T] -> X) -> Term Xという型がつくことで表現される。
（ここで[T]は型TをCPS変換した型）

GADTは表現力の高いDSLであるが、parse :: String -> Maybe (Term T)のような関数を書くことはできないため、標準入力からラムダ項を受け取りcps関数に渡すためには少し工夫がいる。

今回はtypeCheck :: Term' -> A -> (forall T. Term T -> A) -> A
という関数を実装することでこの問題を解決した。

実装は以下で公開されている。github.com

とてもとても簡単な解説

CPS変換の実装はSyntax.hsで、パーズした入力をGADTのラムダ項を生成する部分は
TypeCheck.hsにある。詳細は実装を読んでほしい。後日解説を書くかもしれない。

実行例はこんな感じ

$ ./cpstransformer
\(x::o) -> x
Parsed: \(x :: o) -> x
TypeCheck : OK
CPS : (\(x :: o -> (o -> o) -> o) -> end) (\(x :: o) -> \(k :: o -> o) -> k x) 
\(a :: o) -> (\(x :: o -> o) -> x a) (\(b :: o) -> b)
Parsed: \(a :: o) -> (\(x :: o -> o) -> x a) (\(b :: o) -> b)
TypeCheck : OK
CPS : (\(x :: o -> (o -> o) -> o) -> end) (\(a :: o) -> \(k :: o -> o) -> (\(f :: (o -> (o -> o) -> o) -> (o -> o) -> o) -> (\(x :: o -> (o -> o) -> o) -> f x k) (\(b :: o) -> \(k :: o -> o) -> k b)) (\(x :: o -> (o -> o) -> o) -> \(k :: o -> o) -> (\(f :: o -> (o -> o) -> o) -> (\(x :: o) -> f x k) a) x))
\(x :: o -> o) -> x x
Parsed: \(x :: o -> o) -> x x
TypeCheck : failed

参考文献

今回実装したCPS変換は次のサイトを参考にしている。
How to compile with continuations