TDD本の6章で紹介されていた例が面白かったので、少しだけ変えてより直感的にしてみました。

printf という関数

printf という関数は第一引数に "number is %d, string is %s" のようなフォーマット文字列を受け取り、第二引数以降に %d などで指定したパラメータの値をフォーマット文字列に登場した順に受け取ります。

あんまり色々対応してもめんどいので、今回は %d と %s だけ対応します。それぞれ Int と String をパラメータの型として期待します。

出力までやってもいいのですが¹、とりあえず今回は単に文字列を返すだけにしておきます。

雑に型を考えると

雑に型を考えるなら
printf : String -> List (Either Int String) -> String
みたいにしてもいいのですが、それだと
printf "%d" [Left 3, Right "foo"]
という呼び出しが型の上では正しくなってしまいます。1個しかパラメータが期待されていないのに2個渡しているので、これはコンパイルエラーにしたいわけです。

可変長引数の関数

リストを受け取るようにしてもいいのですが、可変長引数の関数を定義することも可能です。例えば

FunWithNNats : (n : Nat) -> Type
FunWithNNats Z     = Nat
FunWithNNats (S n) = Nat -> FunWithNNats n

とすると、FunWithNNats n で「n個の自然数を引数にとって自然数を返す関数」の型が作れます。この上でさらに

fun1 : (t : Bool) -> FunWithNNats (if t then 3 else 0)
fun1 False = 0
fun1 True  = \a, b, c => a + b + c

とすれば、fun1 は第一引数が False のときはそれ以上引数を取らずに 0 を返し、 True のときはさらに3つの引数をとってそれらの総和を返す関数になります。

Idris では型宣言の部分にもあらゆる式が記述出来るので、上記のように if も書けるわけです。

fun1 False 1 のような関数呼び出しはコンパイルエラーになりますし、
fun1 True 1 2 3 はコンパイルが通ります。

問題は fun1 a 1 2 3 のような関数呼び出しですが、これはなんと a の値がコンパイル時に True であると確定しているときのみコンパイルが通ります。例を挙げると:

a : Bool

x : Nat
x = fun1 a 1 2 3

はコンパイルエラー(fun1 a の型は FunWithNNats (if a then 3 else 0) であって関数型じゃないので関数適用出来ません、というエラー)で、

a : Bool
a = True

x : Nat
x = fun1 a 1 2 3

はコンパイルが通ります。

データ構造を考える

この関数の裏には「フォーマット」という概念があります。まずはこれをデータ構造で表してみましょう。

今回考えるフォーマットは文字列リテラル、%d、%s の3種類のものが並んだものです。コードにすると:

data FormatComponent : Type where
  Literal : String -> FormatComponent
  PD      : FormatComponent
  PS      : FormatComponent

Format : Type
Format = List FormatComponent

ちなみに、この FormatComponent の定義は単に
data FormatComponent = Literal String | PD | PS とも書けます

(%d, %s のつもりで PD, PS という名前にしてます)

printf の型の作り方を考える

printf の返り値(第二引数以降の部分)の型は printf の第一引数のフォーマット文字列の値によって変化します。
従って String を受け取って printf の返り値の型を返す関数を作りたくなるわけですが、フォーマット文字列をそのまま扱うのはだるいので、一旦パースして Format 型の値を経由することにしましょう。すなわち:

パーサー parseFormatString : String -> Format を作る
パースした Format から printf の返り値の型を作る関数 PrintfReturnType : Format -> Type を作る

とすれば、printfの型は

printf : (formatString : String) -> PrintfReturnType (parseFormatString formatString)

と出来るわけです。ここまでの型をまとめると

Format : Type

parseFormatString : String -> Format

PrintfReturnType : Format -> Type

printf : (formatString : String) -> PrintfReturnType (parseFormatString formatString)

となります。あとは実装を埋めるだけですね。

実装を埋める

それぞれ順番にやっていきます。

`parseFormatString`

文字列を左から順に読んでいって、 %d や %s があればそれぞれ PD 及び PS にして、それ以外はリテラルとして結合し続けていけばいいでしょう。

文字列の先頭にパターンマッチさせるのはちょっと面倒なので、まず unpack : String -> List Char で List Char に変換してから処理していきます。

parseFormatString : String -> Format
parseFormatString str = parseCharList (unpack str) where
  parseCharList : List Char -> Format
  parseCharList []                    = []
  parseCharList ('%' :: 'd' :: chars) = PD :: parseCharList chars
  parseCharList ('%' :: 's' :: chars) = PS :: parseCharList chars
  parseCharList (char :: chars)       = ?parseCharList_rhs4

途中まで実装しました。 parseCharList というローカル関数を定義してこの中で再帰呼び出しをしていきます。
リストが空の場合は [] を返せば良いでしょう。
リストの先頭が %d の場合は PD を、 %s の場合は PS を先頭に追加して再帰呼び出しすれば良いです。

問題は他のケース、すなわちリテラルだったときです(ここを ?parseCharList_rhs4 という hole にしています)

ここでは一旦残りの chars をパースして、パースした結果先頭に Literal が来れば char をそのリテラル文字列の先頭に追加する必要があります。それ以外の場合は単に char のみからなるリテラル文字列を先頭に追加すればいいですね。
strCons : Char -> String -> String と cast : Char -> String が使えます。

parseFormatString : String -> Format
parseFormatString str = parseCharList (unpack str) where
  parseCharList : List Char -> Format
  parseCharList []                    = []
  parseCharList ('%' :: 'd' :: chars) = PD :: parseCharList chars
  parseCharList ('%' :: 's' :: chars) = PS :: parseCharList chars
  parseCharList (char :: chars)       = case parseCharList chars of
    Literal str :: xs => Literal (strCons char str) :: xs
    xs                => Literal (cast char) :: xs

これでOKですね。一応動作確認しておきましょう:

Idris> :l Printf.idr
*Printf> parseFormatString "foo %d %s"
[Literal "foo ", PD, Literal " ", PS] : List FormatComponent

`PrintfReturnType`

これは素直に実装すれば出来ます。 Format はリストなので、先頭から順に見ていって

PD や PS なら対応した Int か String を引数にとって再帰呼び出しした型を返す関数型
リテラルなら引数を増やす必要は無いので単に再帰呼び出し
空リストなら最後まで到達したので返り値の String

とすれば良いでしょう:

PrintfReturnType : Format -> Type
PrintfReturnType []                = String
PrintfReturnType (Literal x :: xs) = PrintfReturnType xs
PrintfReturnType (PD :: xs)        = Int -> PrintfReturnType xs
PrintfReturnType (PS :: xs)        = String -> PrintfReturnType xs

printf を実装するために

以上で部品はすべて揃ったはずので、 printf を実装していきます。

まずは与えられたフォーマット文字列をパースするわけですが、次にどうすべきでしょう？
こういうときはとりあえず関数の hole を作ってそれに渡すことにします:

printf : (formatString : String) -> PrintfReturnType (parseFormatString formatString)
printf formatString = ?what_now (parseFormatString formatString)

?what_now の型を改めて考えてみると (format : Format) -> PrintfReturnType format であることに気がつくと思います(時間はかかると思いますが…)。
パースされたフォーマットを受け取って「必要なパラメータを引数にとって文字列を作る関数(=renderer)」を返す関数ですね。
ということで formatToRenderer と名前をつけることにします。

フォーマットはリストなので、先頭から順に読んでいって、リテラルなら文字列を結合、PD や PS なら対応した引数を受け取って文字列に変換して結合していけばいいでしょう。
今まで結合した文字列を覚えておきたいので、 accumulator を引数として追加します²:

printf : (formatString : String) -> PrintfReturnType (parseFormatString formatString)
printf formatString = formatToRenderer "" (parseFormatString formatString) where
  formatToRenderer : (acc : String) -> (format : Format) -> PrintfReturnType format
  formatToRenderer acc []                  = acc
  formatToRenderer acc (Literal str :: xs) = formatToRenderer (acc ++ str) xs
  formatToRenderer acc (PD          :: xs) = \int => formatToRenderer (acc ++ show int) xs
  formatToRenderer acc (PS          :: xs) = \str => formatToRenderer (acc ++ str) xs

Int を String に変換するには show が使えます。

完成

以上で完成です。一応コード全体を載せておきます:

Printf.idris

data FormatComponent = Literal String | PD | PS

Format : Type
Format = List FormatComponent

parseFormatString : String -> Format
parseFormatString str = parseCharList (unpack str) where
  parseCharList : List Char -> Format
  parseCharList []                    = []
  parseCharList ('%' :: 'd' :: chars) = PD :: parseCharList chars
  parseCharList ('%' :: 's' :: chars) = PS :: parseCharList chars
  parseCharList (char :: chars)       = case parseCharList chars of
    Literal str :: xs => Literal (strCons char str) :: xs
    xs                => Literal (cast char) :: xs

PrintfReturnType : Format -> Type
PrintfReturnType []                = String
PrintfReturnType (Literal x :: xs) = PrintfReturnType xs
PrintfReturnType (PD :: xs)        = Int -> PrintfReturnType xs
PrintfReturnType (PS :: xs)        = String -> PrintfReturnType xs

printf : (formatString : String) -> PrintfReturnType (parseFormatString formatString)
printf formatString = formatToRenderer "" (parseFormatString formatString) where
  formatToRenderer : (acc : String) -> (format : Format) -> PrintfReturnType format
  formatToRenderer acc []                  = acc
  formatToRenderer acc (Literal str :: xs) = formatToRenderer (acc ++ str) xs
  formatToRenderer acc (PD          :: xs) = \int => formatToRenderer (acc ++ show int) xs
  formatToRenderer acc (PS          :: xs) = \str => formatToRenderer (acc ++ str) xs

(Syntax highlight が効かないのが惜しい…)

REPLで動作確認してみましょう:

Idris> :l Printf.idr

*Printf> printf "%d: %s" 3 "foo"
"3: foo" : String

*Printf> printf "%d: %s" "invalid" "foo"
builtin:Type mismatch between
        String (Type of "invalid")
and
        Int (Expected type)

ちゃんと不正な呼び出しは型エラーになっていますね。

所感(おまけ)

結構大変だったと思うのですが、これは本来 printf が持つ複雑性の高さを表しているのだと思います。
まあ考えてみれば文字列のパースや可変長引数といった複雑な概念を含むものなので、当然といえば当然でしょう。

正確に型付けするということは、「コンパイラに助けてもらいながらその複雑性と向き合う」ということなのだと感じました。
雑に型付けしてコンパイラをごまかすみたいな事よくありますよね。それはコンパイラの差し伸べる手を跳ね除けて複雑性と向き合うことから逃げる行為なのだと思います。もちろんどちらも良し悪しあると思いますよ。

これが出来るんだったら SQL とか GraphQL とかでクエリ文字列に応じて返り値の型が変化するのも正確に表現することが(少なくとも理論上は)出来るということがわかりますよね。夢が広がる。。

実は PrintfReturnType [] = IO () および formatToRenderer acc [] = putStr acc とするだけでよかったりします ↩
ここで accumulator を使わずにやろうとすると、str ++ formatToRenderer xs のようなコードを書きたくなるのですがコンパイルが通りません。再帰呼び出しした結果は関数の可能性があり、文字列の結合が出来ないためです。このように「途中で型の変わるものを扱うけど結果はある固定の型」というケースでは accumulator を使うのが良さそうですね。 ↩

Idris: printf に型をつける