問題

問. 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つのHListxと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拡張はドンドン使っていきましょう。