Idris: printf に型をつける

[TDD本](https://www.manning.com/books/type-driven-development-with-idris)の6章で紹介されていた例が面白かったので、少しだけ変えてより直感的にしてみました。

# printf という関数

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

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

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

# 雑に型を考えると

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

# 可変長引数の関数

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

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

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

```idris
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` であると確定しているときのみコンパイルが通ります。例を挙げると:

```idris
a : Bool

x : Nat
x = fun1 a 1 2 3
```

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

```idris
a : Bool
a = True

x : Nat
x = fun1 a 1 2 3
```

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

# データ構造を考える

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

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

```idris
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` 型の値を経由することにしましょう。すなわち:

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

とすれば、printfの型は

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

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

```idris
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` に変換してから処理していきます。

```idris
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` が使えます。

```idris
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
Idris> :l Printf.idr
*Printf> parseFormatString "foo %d %s"
[Literal "foo ", PD, Literal " ", PS] : List FormatComponent
```

## `PrintfReturnType`

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

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

とすれば良いでしょう:

```idris
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 を作ってそれに渡すことにします:

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

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

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

```idris
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
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 とかでクエリ文字列に応じて返り値の型が変化するのも正確に表現することが(少なくとも理論上は)出来るということがわかりますよね。夢が広がる。。

[^io]: 実は `PrintfReturnType [] = IO ()` および `formatToRenderer acc [] = putStr acc` とするだけでよかったりします

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