Printf実装を通して学ぶGADTs, DataKinds, ConstraintKinds, TypeFamilies
問題
問. Haskellで以下のようなCライクなprintf函数を実装してください。
> printf ["Hello, ", _s, "\n", "an integer:", _d, "\n", "a float:", _f] ["World!", (10 :: Int), (3.1415 :: Float)] -- 出力結果: > Hello, World! > an integer:10 > a float:3.1415
Cのprinfとは異なり、%dや%fが文字列に直接埋め込まれていません。よって当然型が合わなければ、すなわち printf [_d] [(3.1 :: Float)]
などとかくとコンパイルエラーになってほしいわけです。
解答
私が実装したものが以下にあります。
https://gist.github.com/myuon/9084939
以下ではこのコードについて解説していきたいと思います。
解説
まず、printfの第一引数も第二引数もそれぞれの元の型はバラバラです。今はまだ_d
や_f
の型をどうするかについては考えていませんが、とにかく型が違うということだけ分かればまずはヘテロリストの実装からスタートすることになります。
GADTs, DataKinds
ヘテロリストは全ての型がバラバラなので型を保持するのではなくてカインドを保持するようにします。つまり、普通のリストは型がa
のデータを並べたものですが、今回実装するヘテロリストはカインドが*
のデータを並べたものと考えます。
data HList (as :: [*]) where Nil :: HList '[] (:::) :: a -> HList as -> HList (a ': as) infixr :::
HList
の定義にはGADTとDataKindsが使われています。GADTはデータコンストラクタを函数のように定義できる*1もので、確かに上ではdata ... where
という書き方がされています。
DataKindsは定義したデータコンストラクタを型に、型をカインドに同じ名前のまま持ち上げるものです。分かりやすい例を挙げてみましょう。以下は簡単な型レベル自然数の例です。
data Nat = Zero | Succ Nat -- DataKinds拡張を使うと、以下のようなものも自動で生成される -- data Zero -- data Succ (n :: Nat) -- ただし Zero :: Nat, Succ n :: Nat である
これによって、標準的なリスト型は[]
カインドに持ち上げられ、'[], (':)
というデータコンストラクタを昇格してできた型が作られ、*
カインドをもつ型のリストが使えるようになります。
このことを踏まえれば上のコードは、HList
というデータ型の定義であって、as
という変数はカインド*
をもつ型のリストになっていることが分かります。(:::) :: a -> HList as -> HList (a ': as)
によって、与えられた型をそのままリストに追加しているのが分かります。さらに実際に動かして型を調べてみるとよいでしょう。
> :t Nil Nil :: HList ('[] *) > :t "100" ::: (10 :: Int) ::: Nil "100" ::: (10 :: Int) ::: Nil :: HList ((':) * [Char] ((':) * Int ('[] *)))
TypeFamilies, ConstraintKinds
さて、HList
はShow
のインスタンスにできるでしょうか。HList
に登場する全ての型がShow
のインスタンスであればできそうです。このように型への制限を表すのがConstraintで、それをカインドのレベルで扱えるようにするのがConstraintKinds拡張です。
import GHC.Prim (Constraint) type family All (cx :: * -> Constraint) (xs :: [*]) :: Constraint type instance All cx '[] = () type instance All cx (x ': xs) = (cx x, All cx xs)
TypeFamiliesを使えば型を直接扱う函数を定義できます。これによってAll
という型への制限を表す函数を定義します。cx :: * -> Constraint
の部分に適当な型クラスがきます。例えばAll Show
は、カインド*
のリストxs
に対し、その全ての元がShow
のインスタンスになっているという制限を表すことができるわけです。
コレを使ってHList
をShow
のインスタンスにしてしまいます。
instance (All Show as) => Show (HList as) where show Nil = "[]" show (x ::: xs) = show x ++ ":" ++ show xs -- 実行例 -- > "100" ::: 4.2 ::: 10 ::: [1..5] ::: Nil -- "100":4.2:10:[1,2,3,4,5]:[]
TextFの実装
以上でヘテロリストが実装できました。これを使えば我々の目的であるprintf函数の型も大体見当がつくでしょう。
printf :: HList as -> HList bs -> IO () printf x y = undefined
printfは2つのHList
xとyを受け取って、もしもxの先頭がString
型であれば、それをそのまま出力します。そうでなければ、xの先頭とyの先頭の型があっているか(xの先頭が_d
だったらyの先頭はInt
型であるか)を判断して、合っていればそれを出力します。このようにprintfは型によって実装が変わるので、型クラスの出番です。
class TextF as bs where textf :: HList as -> HList bs -> String
また、printfはIO ()
になって少し扱いにくいので、textf :: HList as -> HList bs -> String
という純粋函数を定義して、それを使ってprintfを実装することにしました。
いよいよ実装です。まずは、それぞれのリストas
, bs
がともに空である場合。
instance TextF '[] '[] where textf _ _ = ""
そして、as
の先頭がString
型かどうかでパターンマッチを行います。
instance (TextF as bs) => TextF (String ': as) bs where textf (x ::: xs) y' = x ++ textf xs y' instance (TextF as bs) => TextF ((x -> String) ': as) (x ': bs) where textf (x ::: xs) (y ::: ys) = x y ++ textf xs ys
as
はString
型のデータか、x -> String
型の函数が入っているということにしました。つまり、_d
や_f
は_d :: Int -> String
, _f :: Float -> String
の型であって、さらに_d 10
や_f 3.1415
などの値が画面に出力されることになります。
よって、このような_d
や_f
はshow
そのものですから、これを定義してあげることにします。
_d :: Int -> String _d = show _s :: String -> String _s = id _f :: Float -> String _f = show
(String -> String
だけは、そのままshow
するとクォーテーションがついてくるのでそのままにしてあります。)
まとめ
以上で、printfの実装が完全に出来ました。 では実際に動かして遊んでみましょう。
> printf Nil Nil > printf ("hello!" ::: _s ::: Nil) ("world!" ::: Nil) hello!world! > printf ("hoge:" ::: _d ::: Nil) (3.1415 ::: Nil) *** 型エラー *** > printf ("hoge:" ::: _d ::: Nil) ((20 :: Int) ::: Nil) hoge:20 > printf ("hoge:" ::: 10 ::: Nil) (Nil) *** 型エラー ***
はい、正しく動いているようです。
なお、問ではこれを printf ["hello","world!"] []
のようにリストカッコを用いて書くように言っていましたが、そのようなリストの表記を使えるようにするGHC拡張として、OverloadedListsが提案されているようです。
また、このprintfをCと同じように可変長引数にすることは頑張ればできると思うのでよければやってみてもいいかもしれません。(丸投げ)*2
GADTs, DataKinds, ConstraintKinds, TypeFamiliesなどのGHC拡張を使えば、このような型レベルプログラミングも比較的[要出典]簡単に実装することができます。便利なGHC拡張はドンドン使っていきましょう。
参考
参考にしたページと参考になりそうなページ
- GHC 7.4.1 の型レベル新機能を使い倒す 〜GADTs、型族 と DataKinds、ConstraintKinds の円環〜 - これは圏です
- 7.11. The Constraint kind
- DataKinds 言語拡張を使って Typed Heterogeneous List とその基本操作を実装してみた - hyoneの日記
- Constraint Kinds for GHC | :: (Bloggable a) => a -> IO ()
*1:各データコンストラクタの像を適当な形に制限するために使うものだと思っていますが正確なところは知りません
*2:型クラスを用いた可変長引数の実装はText.Printfが分かりやすいと思います。