PureScript型レベル計算入門

**型レベル計算**(あるいは**型レベルプログラミング**)は、プログラミング言語の型システムを~~悪用~~**有効活用**して、実行時ではなく**コンパイル時に**任意の計算を可能にするものです。PureScript v0.12ではこの型レベル計算の機能がさらに強化されており、型レベル計算を活用した実用的なライブラリがすでに幾つか公開されています。

たとえば、[purescript-safe-printf](https://github.com/kcsongor/purescript-safe-printf) は**型安全な**`format`/`printf`を実現することができます。

```haskell 
format (SProxy :: SProxy "Hello, %s!") "World"
```

ここで`%s`というフォーマット文字列がありますが、この個数や型が正しいことをコンパイル時に検証することができます。(`SProxy :: SProxy ...`という部分がちょっと冗長ですが……たぶんそのうち何らかのショートハンドが用意されるような気がします)

ほかにも、[purescript-kushiyaki](https://github.com/justinwoo/purescript-kushiyaki) はURLのパースを行い、パラメータとなる部分を**型安全に**取り出すことができます。たとえば次のように`"/hello/{name}/{age}"`のような直感的な文字列でパスを定義して`parseURL`でパースすると、そのパラメータ部分を`name`と`age`というフィールドを持つレコード型で取り出すことができます。

```haskell
  case parseURL (SProxy :: SProxy "/hello/{name}/{age}") "/hello/Bill/12" of
    Left e -> do
      log $ "didn't work: " <> e
    Right r -> do
      assert $ r.name == "Bill"
      assert $ r.age == "12"
```

このとき、変数`r`の型`{ name :: String, age :: String }`がどこにも定義されていないことに注目してください。これは、`"/hello/{name}/{age}"`という部分からコンパイラが自動的に型推論で導き出すのです。

この記事ではPureScriptの型レベル計算を基本的なところから紹介していきたいと思います。

# 型レベル計算　前知識編

## EmptyDataDecls

代数的データ型では通常、`=`のあとに`|`で区切ってその型に含まれるデータを列挙して定義します。

```haskell:実行時計算のための真偽値 
data Bool = True | False
```

```haskell:実行時計算のための自然数
data Nat = Zero | Succ Nat
```

```haskell:実行時計算のためのの2要素タプル
data Tuple a b = Tuple a b
```

実行時計算がデータを計算の対象にするのに対して、**型レベル計算では型そのものが計算の対象になります**。必要なのは型だけであってデータは不要ですから、代数的データ型では何もデータのない型を定義することもできるようになっています。型レベルの真偽値や自然数などを定義してみます。

```haskell:型レベル計算のための真偽値 
data True

data False
```


```haskell:型レベル計算のための自然数
data Zero

data Succ a 
```

```haskell:型レベル計算のためのの2要素タプル
data Tuple a b
```

型レベル計算をするときにデータのある型を使っても構わないのですが、空の型にしたほうが型レベル計算のための型であるという意図がわかりやすいです。Haskellでは`EmptyDataDecls`という拡張を使うとこのような空の型の定義できるようになりますが、PureScriptはこの種のコンパイルフラグは一切なく、デフォルトで空のデータ型を定義することができるようになっています。



## 種

実行時計算ではデータを計算の対象とし、型レベル計算では型を計算の対象とします。そして、実行時計算ではデータを型によって分類しますが、それと同じように型レベル計算では型を**種**によって分類して扱います。通常の型は`Type`という種で表されます。また`Type -> Type`という種を持つものは**型コンストラクタ**であり、これは実行時計算におけるデータコンストラクタに相当するものであると考えればいいでしょう。他にも`Symbol`という型レベルの文字列を表す種が存在します。また、`::`を使うと、実行時の式に型を`::`を与えるような感じで、型レベルでのそれぞれの計算の対象について、種を示すことができます。

```haskell
True :: Type

False :: Type

Zero :: Type

Succ :: Type -> Type

Tuple :: Type -> Type -> Type

TypeString :: Type -> Symbol

TypeConcat :: Symbol -> Symbol -> Symbol

"Hello" :: Symbol

Fail :: Symbol -> Type
```



組み込みの種として`Type`、`Type -> Type`、`Symbol`が存在しますが、それ以外の種を自分で新たに定義することもできます。`foreign import kind`という予約語のあとに、種の名前を書くだけです。

```haskell
foreign import kind Nat

foreing import data Zero :: Nat

foreing import data Succ :: Nat -> Nat
```

## `type`

実行時計算で変数を使って値に名前を付けられるように、型レベル計算では`type`を使って型に名前をつけることができます。

```haskell:実行時計算
one :: Nat
one = Succ Zero

two :: Nat
two = Succ One

three :: Nat
three = Succ Two
```


```haskell:型レベル計算
type One = Succ Zero

type Two = Succ One

type Three = Succ Two
```




## `Symbol`

`Symbol`は言語に組み込みの種で、型レベルの文字列を表しています。型のなかに置かれた文字列リテラルがシンボルになります。

```haskell
type Foo = "Foo" :: Symbol
```




## `TypeString`

組み込みの型コンストラクタ`TypeString`を使うと、型からシンボルを作り出すことができます。

```haskell
TypeString :: * -> Symbol
```






## `TypeConcat`

`TypeConcat`は組み込みの型コンストラクタで、シンボル同士を連結することができます。型レベル計算に於ける文字列の連結です。

```haskell
TypeConcat :: Symbol -> Symbol -> Symbol
```

型コンストラクタに別名をつけることもできますので、実行時計算での文字列の連結に使う`<>`と同じように、型レベルでの文字列結合演算子として`<>`を定義してみます。

```
infixl 6 type TypeConcat as <>
```

これを使うと、任意のシンボル同士を連結することができます。

```
type HelloWorld = "Hello" <> "World"
```



## Proxy

`Proxy`を使うと、データのないデータ型に代理の実行時データを与えて、実行時の計算に使うことができます。

```haskell
data Proxy a = Proxy
```

`Proxy a`には`a`という型変数があるのに、データ自体には`a`のデータを持っていません。このように、型変数があるのにその型変数が表すデータを実際には持っていないようなデータ型を**Phantom Type**といいます。データコンストラクタ`Proxy`は実際には`a`のデータを受け取るわけではないので、データの存在しない`Zero`のような型に対しても`Proxy Zero`という型を持つデータを作り出せます。

```haskell
zero :: Proxy Zero
zero = Proxy 
```

`Zero`の型を持つデータは存在しませんが、`Proxy Zero`のデータならいつでも作ることができるというわけです。具体的な応用については、このあとの実践編をごらんください。


## SProxy

`Proxy`は汎用のプロキシですが、`SProxy`というシンボル専用のプロキシもあります。この`SProxy`なデータを用意してそれに`reflectSymbol`という関数を適用すると、任意のシンボルから実行時の文字列データを取得することができます。例えば次のようにすれば、型レベル計算でシンボル"foo"とシンボル"bar"を`<>`演算子で連結し、そのシンボルを`SProxy`で仮の実行時の肉体を与え、それに`reflectSymbol`を適用することで、型レベルで計算した"foobar"という文字列を`log`で実行時に出力できます。

```haskell
foobar :: SProxy ("foo" <> "bar")
foobar = SProxy

main :: forall e. Eff (console :: CONSOLE | e) Unit
main = log (reflectSymbol foobar)
```













## Fail

`Fail`は言語に組み込みの型コンストラクタで、シンボルを受け取って型を返します。しかしこの型はコンパイラによって特別に扱われ、コンパイルしようとするとエラーになります。

```haskell
Fail :: Symbol -> *
```

要するに型レベル計算におけるエラー表現です。コンパイルエラーになったときのメッセージをカスタマイズするのに使えるようです。




## 型レベル計算における関数

型レベル計算で、型を別の型に対応させるには、型クラスを使えばいいようです。たとえば、

```haskell
class Not a b | a -> b
instance notTrue :: Not True False
instance notFalse :: Not False True
```

この`a -> b`というのがfunctional dependencyというもので、型`a`がわかれば型`b`が決まるという型どうしの対応関係を示すものであるようです。


こうしたインスタンス定義では、インスタンスが重複することがよくあります。このときどのインスタンスを優先するかという順序が重要になってきますが、**インスタンスチェーン**といってインスタンスの順序を明示する方法が導入されました。`else`キーワードでインスタンスをつなぐだけです。

```haskell
class Not a b | a -> b

instance notTrue :: Not True False
else instance notFalse :: Not False True
```




# 型レベル計算　応用編

真偽値を用意しました。

```haskell
data True

data False
```

これらの真偽値の値をシンボルに変換する型レベルの『関数』のようなクラスを定義します。`b`に`b :: Symbol`という制約を加えるのと、`a -> b`という対応を書くのがポイント。

```haskell
class Show a (b :: Symbol) | a -> b
```

先ほどの真偽値をそれぞれシンボルに対応させるインスタンスを書くことで、『型レベルの関数』を実装します。


```haskell
instance showTrue :: Show True "True"
instance showFalse :: Show False "False"
```

この『型レベルの関数』を適用するには、それを制約として持つような型を定義します。この後で

```haskell
foo :: forall a. Show True a => SProxy a
foo = SProxy
```

`forall a`で変数`a`を定義し、`Show True a`で`True`に`Show`を適用した結果を`a`に代入する、みたいなイメージです。


```haskell
main :: forall e. Eff (console :: CONSOLE | e) Unit
main = log (reflectSymbol foo)
```

これで`foo`の型が型推論されますが、`Show True a`には`Show True "True"`というインスタンスが存在するので、`foo :: SProxy "True"`であると型推論されます。この`foo`に`reflectSymbol`を適用すれば、実行時の値である`"True" :: String`が取得できるので、これを`log`で実行時に出力することができます。

こんどは真偽値を反転させてから出力してみます。`Not :: * -> *`を定義して、それぞれの値を反転させて対応させるようにインスタンスを書きます。


```haskell
class Not a b | a -> b
instance notTrue :: Not True False
instance notFalse :: Not False True
```

さっきの`Show`と組み合わせてみます。

```haskell
bar :: forall a b. (Not True a, Show a b) => SProxy b
bar = SProxy
```

これがコンパイルされると、まず型システムが`Not True a`のインスタンスがないか探し、`instance notTrue :: Not True False`を見つけて`a`が`False`であると特定します。それから更に`Show a b`つまり`Show False b`のインスタンスを探しますが、`instance showFalse :: Show False "False"`が見つかるので`b`が`"False"`になります。これで、`a`が`False`、`b`が`"False"`のときにこの関数が存在し、その値の型は`SProxy "False"`であるとわかります。したがって、この`bar`を`reflectSymbol`と`log`で出力させると、`"False"`が出力されます。型レベルで定義した`True`を`Not`で反転し、`Show`でシンボルに変換するという計算ができました。

さらにXorを実装してみます。

```haskell
class Xor a b c | a b -> c
instance xorTT :: Xor True True False
instance xorFT :: Xor False True True
instance xorTF :: Xor True False True
instance xorFF :: Xor False False False
```

せっかくなので、さっきの`Not`と組み合わせてみます。

```haskell
xor :: forall a b c. (Xor True False a, Not a b, Show b c) => SProxy c
xor = SProxy
```

`True`と`False`を`Xor`して、それから`Not`したものは、`False`であるとわかりました。ふむふむ。


自然数も扱ってみます。[Type_arithmetic](https://wiki.haskell.org/Type_arithmetic)で紹介されている方法をすこし改造して使いました。

```haskell
numPred :: forall a. Proxy (Succ a) -> Proxy a
numPred = const Proxy

class Number a where
    numValue :: Proxy a -> Int

instance numberZero :: Number Zero where
    numValue = const 0

instance numberSucc :: Number x => Number (Succ x) where
    numValue x = numValue (numPred x) + 1

three :: Proxy Three
three = Proxy

main :: forall e. Eff (console :: CONSOLE | e) Unit
main = logShow (numValue three)
```

これで`3`が出力されます。`Succ a`からそれが表す実行時の数値を計算するには、`Proxy (Succ a)`をかわりに使って計算するわけです。ややこしいですね。リストとかもやろうかと思いましたが、めんどうくさくなりました。


`TypeString`がうまく動いていない気がします。`Fail`に`TypeString True`を与えた時は動くのですが、次のように`reflectSymbol`で`SProxy (TypeString True)`を出力しようとするとエラーになります。

```haskell
s :: SProxy (TypeString True)
s = SProxy

main :: forall e. Eff (console :: CONSOLE | e) Unit
main = log (reflectSymbol s)
```

github全体で探しても`TypeString`の使用例が[非常に稀](https://github.com/search?q=TypeString+PureScript+&type=Code&utf8=%E2%9C%93)なので、これはバグである気がします。まともに使っている例も[これ](https://github.com/purescript/purescript/blob/ebd7c3cfb2b7ad1133c05bf5b1fd5a3f266413b4/examples/failing/ProgrammableTypeErrorsTypeString.purs)がほとんど唯一。よくわかりません。




# 型レベル計算のためのライブラリとか

* [purescript-typelevel](https://github.com/bodil/purescript-typelevel) 型レベルの自然数と真偽値
* [purescript-type-lang](https://github.com/LiamGoodacre/purescript-type-lang) 型レベルのラムダ計算
* [purescript-type-map](https://github.com/LiamGoodacre/purescript-type-map/) 型レベルのマップ



# さいごに

~~ふーん……。型システムだけでこれだけ計算できるのは、すごいといえばすごいですけど、役に立つ場面は相当に限られそうです。ベクトル型に型レベルで要素数を与えてベクトルどうしを加算するときに同じ要素数であることを保証する、みたいな応用例があるみたいですが、他の応用例があんまり思いつきません。~~  (追記)……と最初は思ったのですが、`RowToList`という型クラスの実装を転機に、ジャスティンさんを始めいろんな人が型レベル計算を使ったライブラリをどんどん試作していて、実用性が見えてきました。

コンパイル時計算ではその計算の過程をデバッガで追うといったようなことができなくて不便きわまりないですし、マクロやテンプレートメタプログラミング、Templete Haskellとかもそうですが、コンパイル時計算なんて好き好んでやるものじゃないと思います。コンパイル時に何か計算を走らせたかったら、型レベル計算なんてしなくてもビルドスクリプトから普通のプログラムを適当に走らせればいいわけで。ただ、コード生成は型安全でないコーディングをしているようなものですし、コンパイル時により多くの静的な検証を行うには型レベル計算が役に立つのは確かです。でも……他の人が書いてくれたライブラリを使うぶんには嬉しいのですが、型レベル計算を多用したライブラリを自分で書きたいとは思いません。変態性が高すぎます。正直あんまり好きではないです。(追記) 型クラス計算を利用したライブラリを自分で書きたくはありませんが、他の人が作ったライブラリを使うぶんには快適です。どんどん使いましょう。

今回書いたコードはgistに貼り付けておきました。

* https://gist.github.com/aratama/fa1c2b51753c0dd15ff162b36b9bd48d
* https://gist.github.com/aratama/316e796a5792a7da040be6754fc51938

# 参考文献

* https://wiki.haskell.org/Type_arithmetic 型レベル計算についての一般的な情報や例は、これが一番参考になりました
* https://github.com/paf31/24-days-of-purescript-2016/blob/master/11.markdown PureScriptに於ける型レベル計算についてはコレと
* https://github.com/paf31/24-days-of-purescript-2016/blob/master/21.markdown コレが参考になります
* https://wiki.haskell.org/Phantom_type Phantom型
* https://wiki.haskell.org/Functional_dependencies fundep拡張
* https://github.com/purescript/purescript-symbols

* https://pursuit.purescript.org/packages/purescript-proxy/1.0.0/docs/Type.Proxy