Haskellにおける型レベルプログラミングの基本(翻訳)

## 概要
IOHKのHaskell及び暗号通貨の集中講義に参加したのですが、その中でも苦戦したのが型レベルプログラミングです。
そんな時に非常に助かったのがMatt Parsons氏のブログにて掲載されていた[Basic Type Level Programming in Haskell](http://www.parsonsmatt.org/2017/04/26/basic_type_level_programming_in_haskell.html)です。是非この記事を翻訳し、日本のHaskellコミュニティの方とも共有したいと本人に伝えたところ、快く承諾を得られましたので以下にその文を掲載させて頂きます。

実装したコードはGitHubにもアップロードしているのでそちらも参照してみて下さい。
https://github.com/HirotoShioi/Basic-Type-Level-Programming

### 注意点
なお私はまだHaskellを始めたばかりなので誤訳、誤解しているところがあるかもしれません。それらを指摘して頂けると非常に助かります！

## 始めに
　近年、型依存プログラミングが盛んになっているし、支持している人は型システムにより多くの情報を取り入れることで実現できる素晴らしいことについていつも話している。これは事実だ。型レベルプログラミングはソフトウェアを設計する上で新しい、興味深いツールを提供してくれる。安全性を保証することがでるとともに、場合によっては型を利用することでパフォーマンスの最適化も可能なんだ。

　僕は読者にこれらの利点を売り込もうとしているわけじゃない。おそらく読者の中には[型依存ニューラル・ネットワーク](https://blog.jle.im/entry/practical-dependent-types-in-haskell-1.html)やIdrisを用いて[型システムでネットワークプロトコルを記述する](http://docs.idris-lang.org/en/latest/st/examples.html)を読んだことがある人もいるだろう。これらの記事を読んで型レベルプログラミングに興味を持てなかった人にはこの記事はオススメしない。一方でもし興味があった上でHaskell, Elm, F#,やML系の言語を知っているなら、この記事はあなたにうってつけだ。

## 型の基本
まずはHaskellにて１行で記述できる**もっとも基本的**なことから始めよう。

```haskell
data Unit = MkUnit
data Bool = True | False
```
　このコードブロックでは2つの新たな型を定義している:`Unit`型と`Bool`型だ。`Unit`型には**値コンストラクタ**である`MkUnit`がある。この型には値コンストラクタ1つしかない上に、引数もないので`Unit`と呼んでいる。

　`Bool`には2つの値コンストラクタがある: `True`と`False`だ。これらも`MkUnit`同様引数をとらないため、定数と似たような振る舞いをする。

　**型**であるというのはどういう意味なのかって？型は物を分類する方法なんだ。「物」では曖昧かもしれない。ここでは「物」とは何を指すのだろうか。

　上記の基本型に関していえば、それぞれの取りうる値を全て定義したことになる。`True`と`False`は`Bool`型の値と言える。また`1`や`a`、`Unit`は決して`Bool`型ではないこともわかる。

　この例では退屈だ。他の型も見てみよう。

```haskell
data IntAndChar = MkIntAndChar Int Char
```

　ここでは2つの引数`Int`、`Char`を取り、値コンストラクタが1つだけの`IntAndChar`型を定義している。この型の値は以下のようになる：

```haskell
theFirstOne = MkIntAndChar 3 'a'
theSecond   = MkIntAndChar (-3) 'b'
```

`MkIntAnChar`はまるで関数のようだ。実際、GHCiにその型を問い合わせると以下のものが得られる。

```console
λ> :t MkIntAndChar
MkIntAndChar :: Int -> Char -> IntAndChar
```

`MkIntAndChar`は`Int`と`Char`を引数に取り、`IntAndChar`型の値を返す関数であることがわかる。つまり値コンストラクタに引数を渡すこと値となり、その値には型があるんだ。では型に引数を渡すことはできるだろうか。もしできたとしたらそれはなんなのだろうか。

## 高階カインド(Higher Kinds)
まず関数と値についておさらいをしよう。型シグネチャが`foo :: Int -> IntAndChar`である関数は以下のことを述べている

> `Int`型の値を渡してください、そうすれば`IntAndChar`型の値を返しますよ。

では次にそれを型レベルに*リフト*しよう。**値**コンストラクタは**値**を受け取り、**値**を返す。つまり**型**コンストラクタは**型**を受け取り、**型**を返すべきだ。Haskellでは**型変数**がこれを可能にする。

ここでみんなが大好きな直和型を例に挙げよう

```haskell
data Maybe a
    = Just a
    | Nothing
```

ここでは2つの値コンストラクタ`Just a`と`Nothing`を持つ`Maybe`型を定義している。`Just`は`a`型の値を引数にとり、`Nothing`は何も受け取らない。ここでGHCiに`Just`と`Nothing`の型を聞いてみよう!

```console
λ> :t Just
Just :: a -> Maybe a
λ> :t Nothing
Nothing :: Maybe a
```

どうやら`Just`は関数型のようだ。そして与えた型の`Maybe`型となる。一方`Nothing`は値も取らずに任意の型になれる。これらで少し遊んでみよう

```console
λ> let nothingA = Nothing :: Maybe a
λ> let nothingInt = Nothing :: Maybe Int
λ> let nothingChar = Nothing :: Maybe Char
λ> nothingInt == nothingChar

\<interactive\>:27:15: error:
    • Couldn't match type ‘Char’ with ‘Int’
      Expected type: Maybe Int
        Actual type: Maybe Char
    • In the second argument of ‘(==)’, namely ‘nothingChar’
      In the expression: nothingInt == nothingChar
      In an equation for ‘it’: it = nothingInt == nothingChar
λ> nothingA == nothingInt
True
λ> nothingA == nothingChar
True
```

ワーオ！ `nothingInt`を`nothingChar`と比較しようとすると型エラーが出力されたぞ。でもこれは理にかなってるんだ。だって`(==)`は型が同じもの同士でしか比較ができないからね。では`nothingInt`と`nothingChar`を`nothingA`と比較したときにエラーが出ないのはなぜだろう?

それは`nothingA :: Maybe a`の実際の意味が

> 私は`Maybe a`型の値です。`a`の取りうる型であれば任意の型になります。

だからだ。
`MkIntAndChar`に値を渡すことと、`Maybe`に型を渡すことは非常に似ているんだ。
ここでGHCIに`Maybe`の型を尋ねてみよう

```console
λ> :type Maybe

\<interactive\>:1:1: error:
    • Data constructor not in scope: Maybe
    • Perhaps you meant variable ‘maybe’ (imported from Prelude
```
どうやら型の型はないようだ(ある意味ではね）。実は型には*カインド(Kind)*があるんだ。`:kind`コマンドによってGHCiに型の*カインド*を尋ねることができる。

```console
λ> :kind Maybe
Maybe :: * -> *
```

この`*`記号は何かって？　`*`は**値を持つ型(具体型)**の*カインド*を意味するんだ。GHCiにて確認してみよう。

```console
λ> :kind Maybe
Maybe :: * -> *
```
`Maybe`の*カインド*が`* -> *`であるということは:
> 具体型を渡してくれれば具体型を返しますよ

ということなんだ。

　もしかしたら読者の中には**高階多相カインド**について聞いたことがある人がいるかもしれない。ここである型を例に挙げてみよう。

```haskell
data HigherKinded f a
    = Bare a
    | Wrapped (f a)
```
Haskellのカインド推論は非常に親切だ。ここでは`a`に`f`を適用しているので、Haskellは`f`のカインドは`* -> *`であることを推論してくれる。ここでGHCiに`HigherKinded`の*カインド*を尋ねてみると

```console
λ> :kind HigherKinded
HigherKinded :: (* -> *) -> * -> *
```
となる。

つまり`HigherKinded`は*カインド*が`* -> *`と`*`の型を受け取り、具体型である`*`を返す型なんだ。くどい説明をすると以下のようになる
> 2つの型をください。1つは具体型ではありませんが、具体型を渡すことで具体型となる関数です。もう1つは具体型です。2つを渡せば私は具体型を返します。

## 動的カインド付けプログラミング
`*`は正規表現の「なんでもマッチする」を思い出させる。`*`は具体型、あるいはその型の唯一の値が無限ループを生み出すものでさえそのカインドは`*`なんだ。

```console
λ> data Void
λ> :kind Void
Void :: *
```
`Void`には値コンストラクタがないが、それにもかかわらずカインドは`*`だ。

*動的型*を用いることで値レベルで効率的なプログラミングを行えることと同様に、*動的カインド*を用いることで型レベルで効率的にプログラミングを行うことが可能となるんだ。

型レベルで数字の記述を行なってみよう。まずはペアノ数の表現からだ。ペアノ数とは自然数を`Zero`、もしくは任意の自然数`Nat`の`Successor`であると定義されている。

```haskell
data Zero
data Succ a

type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ (Succ (Succ (Succ Zero)))
```
一応可能だが、これには納得がいかない。これでは`Succ Bool`のような矛盾した型の定義が可能となるからだ。私は物事を明確にし、エラーを防ぐのが型の利点だと考えているので、型プログラミングを行う際に型の安全性を放棄するのはばかげている。安全性を取り戻すにはどうやら`*`以外のカインドを導入する必要があるようだ。

## Data Kinds
```haskell
{-# LANGUAGE DataKinds #-}
```
言語拡張である`DataKinds`を利用することによって*値*コンストラクタを*型*コンストラクタへ、*型*コンストラクタを*カインド*コンストラクタへ*昇格*することができる。また昇格したものは名前の前にアポストロフィ`'`を付けることで利用できる。

それでは**カインド安全**な自然数の定義を行なってみよう

```haskell
data Nat = Zero | Succ Nat
```
普通のHaskellではこの定義によって、2つの値コンストラクタ、Zero、そしてNat型の値を受け取るSuccを持つ新しいNat型が定義されたことになる。言語拡張`DataKinds`を利用すると新たな定義が加えられる。別の名前空間に存在する新しいカインド`Nat`と、定数型でありカインドが`Nat`である`'Zero`とカインド`Nat`を持つ型を受け取ることのできる型コンストラクタ`'Succ`だ。GHCiにこの2つのカインドを確認してみよう

```console
λ> :kind 'Zero
'Zero :: Nat
λ> :kind 'Succ
'Succ :: Nat -> Nat
```
ここで「なんかこれ見たことあるぞ！」と思った人もいるかもしれない。それもそのはずだ、これらの値の型も見た目上は全く同じように見えるからだ。

```console
λ> :type Zero
Zero :: Nat
λ> :type Succ
Succ :: Nat -> Nat
```
値なのか型なのかが曖昧であるときにはアポストロフィ`'`をつけることによって曖昧さを取り除くことができる。それ以外の場合にはHaskellは推論してくれる。ここで大事なのは`'Zero`型は**具体型ではない**ことだ。カインドが`*`である型のみが具体型となる。
ここでは基本的な型及びカインドを構築した。実際にこれらを利用するには他の言語拡張が必要となる。

## GADTs
```haskell
{-# LANGUAGE GADTs #-}
```
ここで読者の中には「GADTって一体なんの略称なんですか？」と思った人もいるかもしれない。Richard Eisenberg氏なら[Generalized Algebraic Data Typesの略称なんだけど、その用語はあまり役に立たないからGADTsと呼んでくれ](https://www.youtube.com/watch?v=6snteFntvjM)と言うだろう。

GADTsはコンストラクタのパターンマッチングによって型の情報を提供できる言語拡張だ。GADTsではデータ型の構文が通常のHaskellとは異なる。ここで構文がどのように変わるのかを確認してみよう

```haskell
data Maybe a where
    Just :: a -> Maybe a
    Nothing :: Maybe a
```
GADTの構文では値コンストラクタを１行ごとに定義する。また値コンストラクタにフィールドを提供するのではなく、型シグネチャを提供する。これは非常に興味深い変更だ。今`Just`を`a -> Maybe a`と記述することができた。つまりこれは以下の定義が可能になることを意味する。

```haskell
data IntBool a where
    Int :: Int -> IntBool Int
    Bool :: Bool -> IntBool Bool
```
ここでは新たな型`IntBool`型を定義している、そしてその*カインド*は`* -> *`だ。また値コンストラクタが2つある: `Int`は型シグネチャが`Int -> IntBool Int`であり、`Bool`は`Bool -> IntBool Bool`となっている。

値コンストラクタが返り値の型に関する情報を保持するので、値コンストラクタでパターンマッチを行なった際に型に関する情報が得ることができるんだ! これを次の関数で確認してみよう。

```haskell
extractIntBool :: IntBool a -> a
extractIntBool (Int _)  = 0
extractIntBool (Bool b) = b
```
非常に興味深いことが起きた！`Int`でマッチングを行なった際には`IntBool a ~ IntBool Int`であることをGHCがわかっているようだ。この波線`~`は**型同値(Type equality)**であることを意味し、GHCがコードの型チェックを行う際に解決する必要のある*制約*を課したことになる。

これらの言語拡張によりみんなが大好きな型依存を実装することができるようになった: 要素数を型レベルで表現するベクトルだ!

## ベクトル
このベクトルはリストの長さを型レベルで表現するリストだ。これによってリストの`out-of-bounds`エラーを静的に回避することができる。我々は`DataKinds`を利用することによって自然数を型レベルに*昇格*することができた。また`GADTs`によって型の情報を提供できるようになった。次にこれらを組み合わせてみよう。

ここではわかりやすく説明するためにベクトルの定義を複数に分けて行う

```haskell
data Vector (n :: Nat) a where
```
ここで我々はカインドが`Nat -> * -> *`である`Vector`型を定義した。最初の型引数がベクトルの長さであって、2つ目の引数がベクトルに含まれる値の型となる。ここでは**カインド注釈**を行なっているのでコンパイルするには以下の言語拡張が必要となる

```haskell
{-# LANGUAGE KindSignatures #-}
```
型を意識する際に、私たちはしばしば、構築するときには帰納的に、そして分解するときには再帰的に考える必要があっただろう。ベクトルの基底部とはなんだろうか?それは長さが`Zero`のベクトルだ。

```haskell
VNil :: Vector 'Zero a
```

`VNil`によって構築される値は任意の型`a`を持つことができるが、そのベクトルの長さは`'Zero`となる。
帰納的なケースはベクトルに値を追加することだ。値を1つ追加するということはベクトルの長さが１増えるということになる。

```haskell
VCons :: a -> Vector n a -> Vector ('Succ n) a
```
値コンストラクタ`VCons`は2つの値をとる、`a`型と、`Vector n a`型の値だ。渡されたベクトルの長さ`n`は、任意の自然数であって、実際にどれだけ長いのかはわからない。ただ`VCons`が返すベクトルの長さは`n`に1を足したものであることはわかっているので`'Succ n`とすればいい。
以下に完全な注釈を行なった明示的な定義を記載する

```haskell
data Vector (n :: Nat) (a :: *) where
    VNil :: Vector 'Zero a
    VCons :: a -> Vector n a -> Vector ('Succ n) a
```
幸いなことにHaskellはこれらを推論してくれるので、上記の明示的な定義と暗黙的な定義のどちらを使用するかは読者の好みとなる。

```haskell
data Vector n a where
    VNil :: Vector Zero a
    VCons :: a -> Vector n a -> Vector (Succ n) a
```
次にベクトルの**Show**インスタンスを定義しよう。これは簡単だ

```haskell
instance Show a => Show (Vector n a) where
    show VNil         = "VNil"
    show (VCons a as) = "VCons " ++ show a ++ " (" ++ show as ++ ")"
```

## ベクトルのAPI
次にベクトル同士の連結関数`append :: Vector n a -> Vector m a -> Vector ??? a`を定義してみよう。でも待てよ、`???`は一体どうすればいいんだ？ `???`は2つの自然数`n`と`m`の*合計値*であることを表現しなければならない。足し算は*関数*だ。型関数なんてあるのだろうか？まぁ実はあるんだが、それを利用するにはGHCに新たな言語拡張を加えなければならない。

```haskell
{-# LANGUAGE TypeFamilies #-}
```

なぜだか知らないが、型レベルで実行可能な関数は**型族**と呼ばれているんだ。型族の定義方法は２種類ある。**オープン**は誰でも新たなケースを追加できるのに対し、**クローズド**なものは全ての定義づけが一度に行われる。ここではクローズドな型族を扱うことになる。

では、型レベルで2つの自然数を追加する方法を考えてみよう。まずは値レベルで2つの自然数の合計値をどうやって求められるのか、その仕組みを理解しよう。

```haskell
add :: Nat -> Nat -> Nat
```
これはみんなが大好きなHaskellの関数定義だ。ここでは値のパターンマッチ、`where`構文を用いて補助関数を定義することなどができる。

我々は*帰納的*に数値を定義したので、合計値は*再帰的*に求めることができそうだ。これはつまり基底部および帰納的なケースを扱う必要があることを意味する。まずは基本的なことから始めよう。任意の数`n`に0を足せば、その合計値は`n`となる。

```haskell
add Zero n = n
```
帰納的なケースでは以下のことが問われている
> 数（Succ n）の後続(Successor)を別の数（m）に足すと、その答えは何ですか？

`Zero`まで再帰的に求めたいので、数を少しだけ減らしたいわけだ。ここでは左の`Succ`を右の`m`へ移動させる。これで2つの自然数の合計値を再帰的に求められるようになった。

```haskell
add (Succ n) m = add n (Succ m)
```
自然数をお皿を積み上げたものだと想像すれば、自然数の加算というのは1つ目のスタックからお皿を１枚取り、2つ目のスタックに積み上げるようなものだと想像できるだろう。最終的に1つ目のお皿のスタックはZeroとなり、残された唯一のスタックが2つのスタックの合計値となる。

```haskell
add :: Nat -> Nat -> Nat
add Zero n     = n
add (Succ n) m = add n (Succ m)
```
それではこの関数を型レベルに昇格させよう。

## 型族
型族の最初の定義はシグネチャとなる

```haskell
type family Add n m where
```
これによって2つの引数を受け取る型関数`Add`を定義したことになる。次にそれぞれのケースを考えてみよう。ここでは値コンストラクタと同様、型コンストラクタを用いてパターンマッチすることができる。なので基底部`Zero`は以下のようになる。

```haskell
Add 'Zero n = n
```
次に帰納的なケースを再帰的に求めることになる

```haskell
Add ('Succ n) m = Add n ('Succ m)
```
だがここでGHCはエラーを出力する

```console
    • The type family application ‘Add n ('Succ m)’
        is no smaller than the instance head
      (Use UndecidableInstances to permit this)
    • In the equations for closed type family ‘Add’
      In the type family declaration for ‘Add’
```
GHCは決定不能性に非常に怯えており、それが自身で解決できない場合には何もしなくなるんだ。
`UndecidableInstance`は次のような言語拡張となる。

>GHC、大丈夫だよ。お前がこれを解決できないのはわかってる。最終的にこの問題は解決されるから安心してくれ

というわけでこの拡張も追加する。

```haskell
{-# LANGUAGE UndecidableInstances #-}
```
これでコンパイルも通るようになった。この関数をどうやって試せばいいだろうか。

型のカインドを確認するのに`:kind`コマンドを利用したのと同様に、`:kind!`コマンドを使えば型の*評価*を行うことができる。以下のコードではその違いを紹介する

```console
λ> :kind Add (Succ (Succ Zero)) (Succ Zero)
Add (Succ (Succ Zero)) (Succ Zero) :: Nat

λ> :kind! Add (Succ (Succ Zero)) (Succ Zero)
Add (Succ (Succ Zero)) (Succ Zero) :: Nat
= 'Succ ('Succ ('Succ 'Zero))
```
`kind`では2つの自然数(`Nat`)を足すこと(`Add`)は自然数`Nat`であることを示している。一方`kind!`を用いると型関数の評価を行い、その結果を返している。素晴らしい!これで`append`関数を定義することができる

```haskell
append :: Vector n a -> Vector m a -> Vector (Add n m) a
```
まずは型システムがもたらす恩恵を確認するために安易な実装を試みる。

```haskell
append VNil rest = VNil
```
予想通りこれは型エラーが出力される。いい感じだ!

```console
    • Could not deduce: m ~ 'Zero
      from the context: n ~ 'Zero
        bound by a pattern with constructor:
                   VNil :: forall a. Vector 'Zero a,
                 in an equation for ‘append’
        at /home/matt/Projects/dep-types.hs:31:8-11
      ‘m’ is a rigid type variable bound by
        the type signature for:
          append :: forall (n :: Nat) a (m :: Nat).
                    Vector n a -> Vector m a -> Vector (Add n m) a
        at /home/matt/Projects/dep-types.hs:30:11
      Expected type: Vector (Add n m) a
        Actual type: Vector 'Zero a
    • In the expression: VNil
      In an equation for ‘append’: append VNil rest = VNil
    • Relevant bindings include
        rest :: Vector m a
          (bound at /home/matt/Projects/dep-types.hs:31:13)
        append :: Vector n a -> Vector m a -> Vector (Add n m) a
          (bound at /home/matt/Projects/dep-types.hs:31:1)
```
エラーメッセージの量に怖気付いた人もいるかもしれない。これを読み解いてみよう。
GHCは2つ目のベクトルの長さである`m`が`Zero`であることを推論できないと言っている。1つ目のベクトルの長さ`n`は`VNil`のパターンマッチを行なっているので`Zero`であることはわかっているようだ。ではどのような値を返すことができるのだろうか？一度GHCiで型を確認してみよう。

```console
λ> :t append VNil
append VNil :: Vector m a -> Vector m a
```
`append VNil`は返り値として`Vector m a`型の値を返すようになっている。そして我々は`m`が一体何なのか全く知らない。よって引数をそのまま返す必要があるので基底部は以下のようになる。

```haskell
append VNil xs = xs
```
返り値が`Vector m a`型である以上、2つ目の引数をそのまま返す以外の方法を試みると**型エラーによりコンパイルすらできなくなる**。これが型レベルプログラミングの特徴だ。

次に先ほどの自然数の加算と同様、帰納的なケースも扱う必要がある。1つ目の引数の基底部を先ほど定義したので、1つ目を再帰的に呼び出すのが良さそうだ。
まずは安易な実装を試みる

```haskell
append (VCons a rest) xs = append rest (VCons a xs)
```
しかしこれは我々が期待しているような動作はしない。GHCiにて確認してみよう。

```console
λ> append (VCons 1 (VCons 3 VNil)) (VCons 2 VNil)
VCons 3 (VCons 1 (VCons 2 (VNil)))
```
ここでは`VCons 1 (VCons 3 (VCons 2 VNil))`を返すはずだが実際には全く異なるものが返ってきた。ベクトルはその長さを型レベルで表現しているが、どのように連結しているかという情報は保持していない。型レベルに持ち込まれていないものはその正確性が保証されないんだ。
それでは先ほどの実装を修正してみよう。

```haskell
append (VCons a rest) xs = VCons a (append rest xs)
```

次にGHCiにてこれを試してみよう

```console
λ> :reload
[1 of 1] Compiling DepTypes         ( /home/matt/Projects/dep-types.hs, interpreted )

/home/matt/Projects/dep-types.hs:32:28: error:
    • Could not deduce: Add n1 ('Succ m) ~ 'Succ (Add n1 m)
      from the context: n ~ 'Succ n1
        bound by a pattern with constructor:
                   VCons :: forall a (n :: Nat).
                            a -> Vector n a -> Vector ('Succ n) a,
                 in an equation for ‘append’
        at /home/matt/Projects/dep-types.hs:32:9-20
      Expected type: Vector (Add n m) a
        Actual type: Vector ('Succ (Add n1 m)) a
    • In the expression: VCons a (append rest xs)
      In an equation for ‘append’:
          append (VCons a rest) xs = VCons a (append rest xs)
    • Relevant bindings include
        xs :: Vector m a (bound at /home/matt/Projects/dep-types.hs:32:23)
        rest :: Vector n1 a
          (bound at /home/matt/Projects/dep-types.hs:32:17)
        append :: Vector n a -> Vector m a -> Vector (Add n m) a
          (bound at /home/matt/Projects/dep-types.hs:31:1)
Failed, modules loaded: none.
```

なんてこった型エラーだ!どうやらGHCは`Add n (Succ m)`が`Succ (Add n m)`と型同値であることを理解できないようだ。これは`Vector`、`Add`、`append`を並べてみるとその原因がわかる。

```haskell
data Vector n a where
    VNil :: Vector Zero a
    VCons :: a -> Vector n a -> Vector (Succ n) a

type family Add x y where
    Add 'Zero n = n
    Add ('Succ n) m = Add n ('Succ m)

append :: Vector n a -> Vector m a -> Vector (Add n m) a
append VNil xs           = xs
append (VCons a rest) xs = VCons a (append rest xs)
```

`Vector`の帰納的なケースでは`Succ`を積み上げている。また`Add`の再帰的なケースでは、1つ目のスタックを減らしつつ2つ目に積み上げているのがわかる。最後に`append`の再帰的なケースでは2つ目のスタックに積み上げている。エラーがどのようにして発生しているのか型注釈を与えながら調べてみよう。

```haskell
append (VCons a rest) xs = VCons a (append rest xs)
```


|値 |型  |
|---|---|
| VCons a rest  |Vector (Succ n) a |
|xs  |Vector m a  |
| append rest xs | Add n m |
| VCons a (append rest xs) | Vector Succ (Add n m) a |
| 求めている型 | Vector Add (Succ n) m a |

[^1]
ここでは`VCons a rest`の型が`Vector (Succ n) a`であり、`xs`の型が`Vector m a`であることがわかる。`append`が返す型に合わせるためにこれらから`Vector (Add (Succ n) m) a`を結果として返さなければならない。右側は`VCons a (append rest xs)`となっている。`VCons`は`append rest xs`に`Succ`を足した長さを持っており、それは`Add n m`であるはずだ。よって長さは`Succ (Add n m)`となる。残念なことに求めている型は`Add (Succ n) m`だ。

我々は`Succ (Add n m)`と`Add (Succ n) m`が型同値であることはわかっている。しかしGHCはこれを判断できないため、お手上げだと言っている。2つは明らかに同等であるが*構造的*に異なるためにエラーとなるんだ。これは型レベルプログラミングが抱えている大きな問題だ。実装内容が重要であり、安易な実装を試みると大問題につながる。ここでは型族`Add`を修正することにより解決される。

```haskell
type family Add x y where
  Add 'Zero n     = n
  Add ('Succ n) m = 'Succ (Add n m)
```
この関数は`Succ`を取り出し、`VCons`に`Succ`を積み上げるという点において`append`関数の再帰部分と構造的に似ている。

この修正によりコンパイルが通り、`append`関数も正常に機能するようになる。

## つまらないです
**全くその通りだ**。一方でこれに興味を持った読者の人にはこれに関して[より良いチュートリアル](https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell)があるのでそれを読むことをオススメする。次に型レベルプログラミングを利用したより興味深い、実践的な例を挙げてみよう。

## Heterogenous Lists
Heterogenous Listsはタプルのようなものだが、帰納的に定義されている。ここでは型レベルでリストの中身の型を保持することによってリストを安全に利用できるようにする。

Haskellにてリストを型レベルで扱うには、次の言語拡張が必要となる

```haskell
{-# LANGUAGE TypeOperators #-}
```
これによって型レベルで演算子が利用できるようになる。

以下が`HList`の定義となる

```haskell
data HList xs where
    HNil :: HList '[]
    (:::) :: a -> HList as -> HList (a ': as)

infixr 6 :::
```

値コンストラクタ`HNil`は値がないため空のリストとなる。`:::`演算子は、`a`型の値と型のリスト`as`を保持する`HList`をとり、返り値として型レベルで最初の要素が`a`型であり、その後に`as`が続く`HList`を返す。

次にこの`HList`を使ってみよう

```haskell
λ> :t 'a' ::: 1 ::: "hello" ::: HNil
'a' ::: 1 ::: "hello" ::: HNil 
    :: HList '[Char, Int, String]
```
この`HList`ではそれぞれの要素が`Char`,`Int`,`String`であることが型レベルで表現されている。この`HList`を`Show`しようとするとどうなるだろうか。

```console
λ> 'a' ::: 1 ::: "hello" ::: HNil

\<interactive\>:13:1:
    No instance for (Show (HList '[Char, Int, String]))
      arising from a use of ‘print’
    In the first argument of ‘print’, namely ‘it’
    In a stmt of an interactive GHCi command: print it
```

どうやら`HList`の`Show`のインスタンスを定義する必要があるようだね。まずは安易な実装方法としてリストの中身を無視してみよう。

```haskell
instance Show (HList xs) where
    show HNil         = "HNil"
    show (x ::: rest) = "_ ::: " ++ show rest
```
これは全く役に立たない。実際に`Show`のインスタンスを実装する方法はあるのだろうか。もちろんあるさ!

## 帰納的な型クラスのインスタンス
まずは基底部を定義しよう。基底部は空の`HList`だね。

```haskell
instance Show (HList '[]) where
    show HNil         = "HNil"
```
これはコンパイルエラーを起こすので新たな言語拡張を追加する必要がある。

```haskell
{-# LANGUAGE FlexibleInstances #-}
```

上記の型族の定義を行なったファイル以外で`HList`を実装している場合には`FlexibleContext`についてもエラーが発生する。どうやら`UndecidableInstances`を適用すると`FlexibleContexts`も同時に適用されるようだ。念のためにこれも追加しておこう。

```haskell
{-# LANGUAGE FlexibleContexts #-}
```
以上によりコンパイラが通るようになり、`show HNil`が利用できるようになる。次は再帰的な部分の実装だ!
帰納法の原則によると

1. 基底部にて何かをする必要がある
2. 任意の場合でもそれが成り立つと仮定し、1段階上の場合でも成立することを証明する
3. 1と2により、すべての場合にて成り立つことが証明される。

基底部はすでに取り扱ったので、次は任意の場合でも成立すると仮定した上で、その１段階上のものも成り立つことを証明すればいい

```haskell
instance (Show (HList as), Show a) 
    => Show (HList (a ': as)) where
    show (a ::: rest) = 
        show a ++ " ::: " ++ show rest
```

このインスタンスは以下のことを述べている

> 任意の`HList`である`as`を`Show`する方法がわかっていると仮定し、その上で`a`の`Show`のインスタンスがわかっている場合、`a`と`as`を組み合わせた`HList`の`Show`インスタンスも存在する

```console
λ> 'a' ::: 1 ::: "hello" ::: HNil
'a' ::: 1 ::: "hello" ::: HNil
```

### 練習問題
HListの[aeson](https://hackage.haskell.org/package/aeson)のインスタンスを定義せよ。これは先ほど定義した`Show`のインスタンスと似ているが、少し工夫が必要だ。

## 拡張可能レコード
Haskellの拡張可能レコードにはいくつか種類がある。ここでは小規模の実装を行うがそのためにはまた言語拡張を追加しなければならない

```haskell
{-# LANGUAGE PolyKinds        #-}
{-# LANGUAGE TypeApplications #-}
```

`PolyKinds`は型変数の定義を一般化し、これによって具体型のない型変数のカインドを多相カインドにする。また`TypeApplications`は`@`シンボルを利用することにより多相関数に対して明示的に型を渡せるようになる。[^2]

まずフィールドの型を定義し、その上でレコードを定義しよう

```haskell
newtype s >> a = Named a

data HRec xs where
  HEmpty :: HRec '[]
  HCons  :: (s >> a) -> HRec xs -> HRec (s >> a ': xs)
```
引数`s`はカインドが`Symbol`の型だ。`Symbol`は`GHC.TypeLits`にて定義されているので、インポートする必要がある。

次に`TypeApplication`構文を利用して値を構築してみよう。拡張レコードは以下のようになる

```console
λ> HCons (Named @"foo" 'a') (HCons (Named @"bar" (3 :: Int)) HEmpty)

\<interactive\>:10:1: error:
    • No instance for (Show (HRec '["foo" >> Char, "bar" >> Int]))
        arising from a use of ‘print’
    • In a stmt of an interactive GHCi command: print it
```
いい感じだ。まだ`Show`のインスタンスがないのでそれを実装しよう。
フィールド名は型レベルでのみ存在するが、`KnownSymbol`型クラスにある`symbolVal`関数を利用することで値レベルに変換することができる。

```terminal
λ> :t symbolVal
-- proxyを受け取って、その型をStringとして返す
symbolVal :: KnownSymbol n => proxy n -> String
λ> let a = (Proxy :: Proxy "hello")
λ> symbolVal a
"hello"
```

基底部は以下のようになる

```haskell
instance Show (HRec '[]) where
  show _ = "HEmpty"
```

再帰部にはもう少し情報が必要だ。まずは`head`の`Show`インスタンスから始めよう。以下の変数が必要であることはわかっている

```haskell
instance Show (HRec (s >> a ': xs)) where
```

ここではカインドが`Symbol`である型`s`と、具体型`a`そして`xs`がある。次にパターンマッチを行おう

```haskell
instance Show (HRec (s >> a ': xs)) where
    show (HCons (Named a) rest) =
```

まずは`a`の値を`show`したい。これは型クラス制約`Show a`をインスタンスに追加すればだけなので簡単だ。

```haskell
instance (Show a) 
    => Show (HRec (s >> a ': xs)) where
    show (HCons (Named a) rest) =
        let val = show a
```

次に`key`を文字列として表現する必要がある。つまり`s`が型クラス`KnownSymbol`のインスタンスがあると仮定する必要がある。その上で`proxy s`を受け取り、`String`を返す`symbolVal`を利用すればいい。

```haskell
instance (Show a, KnownSymbol s) 
    => Show (HRec (s >> a ': xs)) where
    show (HCons (Named a) rest) =
        let val = show a
            key = symbolVal (Proxy :: Proxy s)
```

この時点で`No instance for 'KnownSymbol s0'`というエラーメッセージが表示された人もいるだろう。これは、Haskellの型変数のスコープがデフォルトでは非常に狭いためだ。例えば以下の例では

```haskell
topLevelFunction :: a -> (a -> b) -> b
topLevelFunction a = go
  where
    go :: (a -> b) -> b
    go f = f a
```

Haskellは各型シグネチャの型変数はそれぞれのスコープがあると解釈する。これは補助関数`go`の変数`a`と`b`は`topLevelFunction`のものと異なるスコープにあることを意味する。よりわかりやすく記述すると以下のようになる

```haskell
topLevelFunction :: a0 -> (a0 -> b0) -> b0
topLevelFunction a = go
  where
    go :: (a1 -> b1) -> b1
    go f = f a
```

型変数が他の変数と同様のスコープを持つようにするには、次の言語拡張が必要となる。

```haskell
{-# LANGUAGE ScopedTypeVariables #-}
```

最後に、残りの部分を実装しよう

```haskell
instance (Show a, KnownSymbol s, Show (HRec xs)) 
    => Show (HRec (s >> a ': xs)) where
    show (HCons (Named a) rest) =
        let val = show a
            key = symbolVal (Proxy :: Proxy s)
            more = show rest
         in "(" ++ key ++ ": " ++ val ++ ") " ++ more
```

以上により非常に納得のいく`Show`のインスタンスができた

```console
λ> HCons (Named @"foo" 'a') (HCons (Named @"bar" (3 :: Int)) HEmpty)
(foo: 'a') (bar: 3) HEmpty
```

### 練習問題
JSONオブジェクトに変換するために`HRec`型のAeson`ToJSON`インスタンスを実装してみよう。
ボーナスポイント: `HRec`型のAeson`FromJSON`インスタンスを実装してみよう。

[^1]: 文章ではわかりにくいと思ったのでテーブルにまとめました。
[^2]: PolyKinds、Proxyに関しては[About kind system of Haskell (Part 1)種の仕組みとそれに付随する言語拡張について](https://haskell.jp/blog/posts/2017/10-about-kind-system-part1.html)を参照してください。