Carrotの変な型システムについて

年末年始は結局だらだらと本を読んで過ごしてて全然Carrotを触ってなかった。昨日今日と頑張ったらとりあえず動く型チェッカができて、わりかし欲しいものに近付いた気がする。

今はCarrotを、クロージャといくつかの基本型しかない、型なしλ計算計算機みたいな抽象機械で動かしてるので、代数的データ型っぽいことをやるのに一工夫必要で、不思議な型システムができた。

概要はこのまえアドベントカレンダーのときに書いた通り、部分適用状態のクロージャに型を付けるというアイディアをベースにしていて、例えばリストならこんな風になる。

;; コンストラクタ
;; {:expr (^ f (f x xs)) :env {x ? y ?}}という形のクロージャが(List a)と型付けされる
(= (cons a (List a) (List a))
   x xs f (f x xs))
(= (nil (List a)) 'nil)

;;アクセサ
(= (car (List a) a) 
   xs (xs true))
(= (cdr (List a) (List a))
   xs (xs false))

多分Haskellみたいにdataっていう文法を追加してやるほうが綺麗に書けるんだけど、文法を増やすのが嫌いなので関数定義文がデータ型の宣言も兼ねるようにした。こうすると型はしっかり抽象的になるんだけど、必然的にデータ型のランタイムでの表現方法は自分で考える事になる。

ランタイムは基本型以外は完全に型なしなので、関数の型宣言は型チェッカを満足させるためだけにあるってことになる。つまりCarrotの型システムはバグ事前発見機以上のものではないってこと。

型システムとランタイムが完全に分離されているので、こんなことができる。

;;;;;;;;;;;;; 透明な箱 ;;;;;;;;;;;;;

(= (put a (Box a))
   x x)                     ;;ただのidentity

(= (take (Box a) a)
   x x)                     ;;これもidentity

(put 8)                     ;;=> 8
(take 8)                    ;;~> Type contradiction: (Box a) -><- Number
(take (put 8))              ;;=> 8

putの実体はa -> aだけど、a -> (Box a)という型が付いているので、(put 8)の結果は8 :: (Box Number)という不思議なことになる。まあさっき書いたようにランタイムは型なしだから8 :: (Box Number)なんて表示は出ないけど。
ランタイムで数値が返るからといって、takeに数値をそのまま渡すと、Numberと(Box a)のユニフィケーションに失敗して、ちゃんと型エラーになる。
(take (put 8))みたいに一度(Box Number)にしてやってからtakeに渡せば8 :: Numberが返ってくるってわけ。

型の上での矛盾はないし、実装もわざわざ変なコンテナに入れなくていいので嬉しい。

問題点は割とあって、例えば、真偽値はa -> a -> aな関数にして、型はBoolにしたいけど、そうしちゃうと=cを使っても分岐の左右が同じ型かのチェックができなくなっちゃう、など。将来的に総称関数とMOPの仕組みができたらクロージャでデータ構造を表す利点ていうのはほとんどなくなる予定なのでこの型システムはそれまでのつなぎになるのかもしれない。

総称関数の静的な解決は、惜しいとこまで行ったんだけど再帰する総称関数に手こずっていったん保留してる。

そうそう、あとI/Oが半年ぶりくらいに動くようになった。遅延評価だから順番がめちゃくちゃになったり、名前呼び出しだったときは同じreadが何回も走ったりと散々だったんだけど、timed-ioっていうのを発明して解決した。

純粋関数型で遅延評価な環境でのIOが難しいのは、まずそもそも文がなくて、プログラム全部が一つの式にならなきゃいけない上に、必要になるまで式の各部分が評価されないから。入出力とかみたいに順番が重要なことをするには一工夫必要。

例えばこんな式があったとしたら、

(= (print String Unit) s (** print s))
(= (read String) (** read))
;; (** hoge x...) はx...を引数にしてホスト言語の関数hogeを呼ぶ

(-> (print "こんにちは、なんて名前ですか?")
 -> (^ _ read)
 id (^ name (-> (print (+++ "よろしく" name "! 好きな物はなに?"))
             -> (^ _ read)
             id (^ thing (print (+++ thing "が好きな" name)))))

printの結果が使われてないからそもそもprintが走らなくてなにも表示されないし、必要呼び出しならいいけど名前呼び出しだったら最後の(+++ thing "が好きな" name)のところでthingだけじゃなくてnameまでもう一回入力しなくちゃ行けなくなるみたいなめちゃめちゃな感じになる。そしてreadは呼ぶ度に違う値を返すから参照透明性が失われる。

そこで、

• printみたいに結果が必要ない関数は、呼ぶ度に固有の数値を返すようにする
• readみたいに入力が要らない関数は固有の数値を取って、それを鍵にして結果をキャッシュする
• print系も数値を取ってキャッシュするようにしとくとなおよし

ということをやると、魔法のように全ての問題が解消する。

(= (print Number String Number) x s (** cached-print x s))
;; (define (cached-print x s) (print s) (+ x 1)) <-- ホスト言語の関数.キャッシュは省略

(= (read Number String) x (** cached-read x))
;; (define (cached-read x) (read)) <-- ホスト言語の関数.キャッシュは省略

(-> (print 0 "こんにちは、なんて名前ですか?")
 -> read
 id (^ name (-> (print 1 (+++ "よろしく" name "! 好きな物はなに?"))
             -> read
             id (^ thing (print 2 (+++ thing "が好きな" name))))))

こうすると、入出力系の関数は毎回違う引数で呼ばれることになるし、同じ引数で呼ばれたらキャッシュされた結果が返却されるから参照透明性は崩れないし、printの結果の数値をreadの入力にしてやることでprintを(readよりも先に)評価する必要が出てくるし、今のCarrotの抽象機械は必要呼び出しだから関係ないけど、名前呼び出しのときにreadが複数回呼ばれる問題もキャッシュ機構のおかげで回避できる。

ちなみにコード中で使った->は、a -> (b -> c) -> (a -> b) -> c)なただの関数で、これで式を繋げて行くとF#の|>とかClojureの->>みたいに使える。マクロなしでも意外と色々変な事できるもんなんだぜ?

と、いうわけです。