Cayenneを実際に使う
"A paper on Cayenne"を見ただけでは全然意味が分からなかったので、
http://www.cs.chalmers.se/~augustss/cayenne/interp.ps
を読んだ。成る程ちょっとdependent typeの事が分かった。
上の論文ではCayenneを使ってinterpreterを作る流れを見せています。
メモのようなもの
型付け言語で書かれるインタプリタの返値は、tagged unionで表される事が普通だが、こいつは非効率だ。
というのも、返す時にはtaggingしないといけないし、値を取り出す時には当然untaggingしなければならない。
Cayenneではdependent typeを上手く使ってtaggingとか無しで勝負してみる、とか言うのがあぶすと。
実際例として、Haskellだと
data Expr = EBool Bool | EInt Int | EAdd Expr Expr data Value = VBool Bool | VInt Int | VError
という感じになる。けど実際の話VBoolとかuntaggingするのが面倒くさい。
上記の型に従って書かれたinterp関数は
interp :: Expr -> Value interp (EBool b) = VBool b interp (EInt i) = VInt i interp (EAdd e1 e2) = case (interp e1, interp e2) of (VInt i1, VInt i2) -> VInt (i1 + i2) _ -> VError
tag unionが役に立つのは次の2点においてで、
- 返値をunion typeの押し込むので、結果的にsingle typeにする事が出来る。
- interpreted programが型安全であることを保証する。
とかいう事。
だけど上のinterp関数は型安全で有る事が分かっている状況下では
interp (EBool b) = b interp (EInt i) = i interp (EAdd e1 e2) = interp e1 + interp e2
とかいう事がしたいんだけど、こんな事すると返値の型がsingle typeじゃないので強い型付け言語(HaskellとかSML)では怒られてしまいますよと。
一方LispとかErlangでは出来る。(dynamically typed languageだし)
でこの問題を解決する為にCayenneではこんな事が出来ますよ、という話。
Cayenneのコード interp :: (e :: Expr) -> TyoeOf e interp (EBool b) = b interp (EInt i) = i -- ただしEAddは動かない。 TypeOf :: Expr -> # TypeOf (EBool _) = Bool TypeOf (EInt _) = Int TypeOf (EAdd _ _) = Int
ここではTypeOfがキモで、こいつを導入した事でValueを駆逐する事が出来た。
#は"Type Of Type"を表している。Javaでいう所の基底Objectみたいな感じなのかしら?
で、EAddが動かない理由っていうのはinterpはBoolもIntも返しちゃうのでEAddにとってはwell typedでは無いから。
この後はEAddを上手く動かす為に色んなものを導入していくけど、重要なのはCayenneにおいて"type is first class value"だ！という事。
もうちょっと面白い例としては
extendV g r x t v = \(x' :: Symbol) -> IF (x == x') v (r x) -- IFは型を返すpredicate
とかこんなの。
"Type is first class value"にする事で、中々に面白い事が出来るなーとか思った。
後、このinterp周りのコードは、Cayenneのtar.gzを取って来て解凍した中に含まれているtest/の中にtinterp/,tinterp_pe/というのがあって、その中に実際のコードが書かれている様子。
型とか
はぶっちゃけ動的型の方が好きに書けちゃって良いとか思っていた、というか考えた事も無かったけどこうやって触れてみると色んな解釈の仕方や使い方があって実に面白いなーとか。
この辺の話をもっと知りたく成ったらTAPL読むという事なのかな。
あと
驚いたのは、この前のprintf関数があれで完結していたという事。
すげーなー。
