Cayenne

が、まずAgdaに先立つんじゃないかと思ったので、遠回りながらCayenneからやっています。

で、Cayenneの面白さはHaskell(少なくともfunctional language)を知っているのと、型理論とかにある程度以上明るいと良いのですが、私は前者はなんとかなってるとして後者がちんぷんかんぷんなのでやれやれ困ったものですという感じで。

Cayenneのページ
http://www.cs.chalmers.se/~augustss/cayenne/

で、tarボール開いた後にmake && make installするわけですが、ちょっと手を加えないといけない所とかが在りつつも上手く導入しました。

取りあえずこれがCayenneっぽいコードを論文から。
http://www.cs.chalmers.se/~augustss/cayenne/paper.ps

PrintfType :: String -> #　-- #はtype of type
PrintfType "" = String 
PrintfType ('%':'d':cs) = Int -> PrintfType cs 
PrintfType ('%':'s':cs) = String -> PrintfType cs 
PrintfType ('%': _ :cs) = PrintfType cs 
PrintfType ( _ : cs) = PrintfType cs 

printf :: (fmt::String) -> PrintfType fmt
printf fmt = pr fmt ""


pr :: (fmt::String) -> String -> PrintfType fmt

pr ""           res = res
pr ('%':'d':cs) res = \(i:Int) -> pr cs (res ++ show i)
pr ('%':'s':cs) res = \(s:String) -> pr cs (res ++ s)
pr ('%':c:cs)   res = pr cs (res ++ [c])
pr (c:cs)       res = pr cs (res ++ [c])

Cayenneのコード

Cayenneでは"型"がfirst class typeです。

printf,prを同じ感じでHaskellで書こうと思うと結構骨が折れます。