GADTs

http://okmij.org/ftp/Haskell/PrintScan.hs
元はコレ。

で、sprintfの所だけ抜き出した

{-# LANGUAGE GADTs #-}

data F a b where
    FLit :: String -> F a a
    FInt :: F a (Int -> a)
    FChr :: F a (Char -> a)
    (:^) :: F b c -> F a b -> F a c

intp :: F a b -> (String -> a) -> b
intp (FLit str) k = k str
intp FInt       k = \x -> k (show x)
intp FChr       k = \x -> k [x]
intp (a :^ b)   k = intp a (\sa -> intp b (\sb -> k (sa ++ sb)))

sprintf fmt = intp fmt id

良ー分からんなぁ。

GADTsの参考
http://www.kotha.net/ghc_users_guide_ja/data-type-extensions.html

これあれか

data F a b where ...

のbは関数の型で、aはbが最終的に返す値の型
とかか。
すると、結合関数(:^)がどうなってるかっていうと。
第一引数で(cという返値の型がbとなる関数)、第二引数で(bという返値の型がaとなる関数)を取るっていうのはなんとなく分かる。

・・・ふむ。

printf色々実装して思うのは

type dependencyなのが宜しいかなーという感じですにゃ。

そこでAgdaだーみたいな事をやりたいんですけどどど。