型レベルプログラミング実践ガイド

この記事は、[PureScript Advent Calendar 2024](https://qiita.com/advent-calendar/2024) の 5日目の投稿です。

この記事では、PureScriptにおける **型レベルプログラミング(Type-level Programming)** について、入門者向けに解説を行います。
難解とされ、時に*Black Art* (†黒魔術†)とも称される型レベルプログラミングですが、"値レベル"プログラミングと適切に対比させて１つずつ理解すれば、そこまで難しいことはやっていないということがわかっていただければ嬉しいです。
記事の後半では、実践例として単純型付ラムダ計算(Simply Typed Lambda Calculus)の型検査器を型レベルプログラミングで実装します。

# 型レベルプログラミングのメンタルモデル

:::note info
「型レベルプログラミング」という言葉をすでに知っていて、PureScriptにおける型レベルプログラミングのやり方が知りたいという方は、このセクションは飛ばしても問題ありません。
:::

型レベルプログラミングを語る前に、まず通常のプログラミングを考えてみます。
ちなみに、型レベルプログラミングの文脈で語るときは、「型レベル」との対比を明示的にするために「値レベルプログラミング」という言い方をすることもあります。

プログラミングの基本は、「**与えられた値から新しい値を計算する**」ことです。私達はそれを計算とよんでいます。
そして計算を構成するのは「**関数**」です。
関数とは、値を受け取るとその値から計算される新しい値を返すものです。
ふつう、関数はどんな値でも受け取れるわけではありません。
そこで、「**型**」によって値を分類し、関数はある特定の型からまたある型への関数というような言われ方をします。
また、この計算が行われるのは **実行時**です。
たとえばブラウザであれば、JSファイルがブラウザにロードされて実行されるときなどです。
一方、「型による値の分類」はコンパイル時に行われるもので、実行時には型は消滅しています。

そこで、我々は「値（関数も含む）たちと型たちは世界の異なる階層に属している」と考えます。
一番低いレベルの階層が「値の世界」で、この世界の住人は42、"x", \x -> x + 1など、実行時に存在するものです。
その１階層上のレベルが「型の世界」で、この世界には`Int`や`Boolean`などの型や、`Array`など型コンストラクタが住んでいます。そして、１階層下の世界の値を分類する役割を担っています。

このような事情は以下のように図示できます:
```
型                \ コンパイル時
↓ 分類             |
↓　　　　　　     　/
値 ------> 値     \ 実行時
    関 数         |
                 /
```

型レベルプログラミングでは、階層が１つ上がって、**型の世界が計算の対象になります**。
すなわち、型レベルプログラミングにおける「関数」は、型を受け取って型を返すものです。
また、型から上の世界は実行時に存在しないので、この「型の計算」はコンパイル時に行われます。
PureScriptでは、あとで詳しく述べるように「型の型」とでもいうべき、型を分類する「カインド」という概念がありますから、型レベルプログラミングは以下のように図示されるわけです。

```
カインド                   \
↓分類                      | コンパイル時
型 --------------> 型      |
    "型レベル関数"　　　　　　/
```

これが、先程の値レベルプログラミミングの図と同じよう形をしていることに注目してください。
型レベルは
 - 値 => 型
 - 型 => カインド
 - 関数 => 「型レベル関数」
 
と、レベルを１つシフトさせ、それぞれのレベルの登場人物をうまく対応付けてやれば、
型レベルプログラムも値レベルのプログラムとほぼ同様に捉えることができるのです。
こう考えれば、一見すると闇の呪文のような型レベルプログラムも、普通に読み書きができるようになるはずです。

それでは、「型レベルの関数」とはPureScriptの言語機能としては具体的に何にあたるのでしょうか？
次にこれを考えてみます。

# 型レベルの"関数"

それでは、型レベルの関数とはなんでしょうか？
通常の値レベルプログラミングで考えると、関数とは値に対して値を対応させるものです:
```purs
incr :: Int -> Int 
incr x = x + 1      -- Intの値xに対して、x + 1という値を対応付ける
```

我々が欲しているのは、型に対して型を対応させるものです。
「指定された型に対して型を対応付ける」という計算を「コンパイル時」に行う仕組みです。

実は、**型クラス ──それもFunctional Dependency(fundep)を持つ型クラス── のインスタンス解決がこの役割を果たします**！

具体例でみてみましょう。fundepを持つ型クラスで身近な例は、transformersライブラリで提供されている `MonadThrow`等の型クラスです。

```purs
class Monad m <= MonadThrow e m | m -> e where
  throwError :: forall a. e -> m a
```

`m -> e` の部分がfundepで、これは「MonadThrowのインスタンスを解決する際は、`m`の型情報だけを使い、`e`の型は`m`から自動的に決まらなければならない」ことを意味しています。

たとえば、`Effect`モナドは `Effect.Exception`モジュールの `Error`型(JavaScriptにおける`Error`のPureScriptバインディング)とともに`MonadThrow`のインスタンスになっているので:

```purs
instance MonadThrow Error Effect where ...
```

以下のように`Effect`の文脈で `MonadThrow` の関数が使用されているとき、PureScriptのコンパイラは `Effect` の `MonadThrow` インスタンスを参照することで、`error` の型が `Error` であると知るわけです

```purs
import Effect.Console as Console

f :: Effect Unit
f = do
  Console.log "foo" -- この行から, PureScriptはEffectコンテキストの中であることを知る
  throwError e      -- すると、Effect の MonadThrowインスタンス宣言からeの型はErrorであることを知る
```

これがfundepを持つ型クラスのインスタンス解決の仕組みです。

これって、見方を変えると
「`Effect`型に対して`Error`という型を対応付けている」
と解釈することができます。

すなわち、**型クラス宣言こそ型から型への"関数" であり、その本体はインスタンス宣言に対応する**、というわけです

```
-- 型レベル関数Foo。１つ引数を受け取って、１つ戻り値を返す。
class Foo a b | a -> b 
-- 型レベル関数Fooの本体 (Tを受け取るとSを返し、 Uを受け取るとVを返す)
instance Foo T S
instance Foo U V

-- cf: 通常(値レベル)の関数だと以下に相当する
foo :: Any -> Any 
foo t = s 
foo u = v
```

# 型レベルプログラミングにおけるプリミティブ

PureScriptでは、特に型レベルプログラミングのためのライブラリ等を使わなくても、
プリミティブな型レベル関数が豊富に用意されています。

### カインド`Type`

Int, Booleanのような型は、42, trueのように実行時に存在できる値が属する型です。
このような型は、すべて `Type`というカインドに属しています。

### 型レベルの整数・ブール・文字列

PureScriptでは、 `42`, `True`, `"foo"`のような**型**を扱うことができます。
これらは、型レベルの整数やブール値、文字列で、それぞれ`Int`, `Boolean`, `Symbol`というカインドに属する型です。
これらを扱う型レベル関数は、それぞれ`Prim.Symbol`, `Prim.Boolean`, `Prim.Int` モジュールで用意されています。これらのモジュールは自動でインポートされないため、使用する際は明示的にインポートする必要があります。

たとえば以下は、`Prim.Symbol`モジュールで定義されている型レベル関数`Append`を使った型レベル関数の例です:

```
import Prim.Symbol (class Append)

class :: Symbol -> Symbol -> Constraint
class Greet name out | name -> out

instance greetImpl :: 
  ( Append "Hello, " name out1 -- 入力の型 name に "Hello, "を左から結合して、結果を型変数out1に束縛
  , Append out1 "!" out        -- out1の右から"!"を結合して型変数 out に束縛
  ) => Greet name out　　　　　  -- 型変数 out を戻り値とする
```

この型レベル関数は、以下の値レベル関数に対応しています：
```purs
greet :: String -> String
greet name =
  let 
    out1 = "Hello, " <> name
    out = out1 <> "!"
  in 
    out
```

再帰的な型レベル関数を書くこともできます。
以下は、型レベル整数`n`を与えられると、`1` 〜 `n`までの整数の和を計算する型レベル関数です:

```purs
import Prim.Int (class Add)

class Sum (n :: Int) (sum :: Int) | n -> sum 

instance sum :: 
  (SumGo n 0 out) => Sum n out

class SumGo (n :: Int) (acc :: Int) (sum :: Int) | n -> sum 

instance sumGo0 ::
  SumGo 0 acc acc 

else instance sumGoN ::
  ( Add n (-1) n'
  , Add acc n acc'
  , SumGo n' acc' out
  ) => SumGo n acc out
```

末尾再帰にするために補助的な型レベル関数`SumGo`を作っていることに注意してください。
`Add`は`Prim.Int`モジュールで提供される、型レベル整数同士の和を計算するための型レベル関数です。

ところで、ここで`else instance`という構文を使っています。
これは、インスタンス宣言 `sumGo0` と `sumGoN` は、それぞれインスタンスヘッドが `0`, `n`となっていて、これらがオーバーラップしている (`n`は`0`の場合をも含んでいる)ため、
そのままでは個々にインスタンス宣言を書くことができないからです。
このような場合は　else instance を使って、上から順番にインスタンスヘッドがマッチするか見ていき、初めにマッチしたインスタンスに解決させることができます。(instance chainというそうです)

**🗒️ 問題**
上記のSumに対応する値レベルの関数を書いてください。
<details><summary>解答</summary>

```purs
sum : Int -> Int 
sum n = sumgo n 0 

sumGo :: Int -> Int -> Int 
sumGo 0 acc = acc
sumGo n acc = 
  let 
    n' = n + (-1)
    acc' = acc + n
  in 
    sumGo n' acc'
```
</details>

### RowとRowList

値レベルプログラミングでのArrayに相当する、１次元のデータの列を表す型レベルのデータが`Row`と呼ばれる型です。

実際には、Rowは１つのカインド`k`を受け取るとカインド`Row k`を作る"カインドコンストラクタ"というべきものです。

`Row Type`は、「順序を持ったラベル付き型の配列」のような型で、たとえば以下のような型が`Row Type`カインドに属します:
```purs
type A = ( foo :: Int, bar :: String )
```
`Row` は配列のようにランダムアクセスが可能なデータ構造で、たとえば以下のように`Prim.Row`モジュールで定義される `Cons` 型レベル関数を使うと、ラベル`k`に対する型を取り出すことができます
```
import Prim.Row as Row

class GetAt :: forall k. Symbol -> Row k -> k -> Constraint
class GetAt k row out | k row -> out 

instance getAt ::
  ( Row.Cons k out rest row -- row において ラベル k に対する型をoutに、kを除いた残りの行をrestに束縛する
  ) => GetAt k row out 
```

値レベルプログラミングで、配列がそのままではパターンマッチして再帰的な関数を書けないのと同様に、Rowに対して再帰的な処理を書くことはできません。

そこで、値レベルの `List` に相当する型 `RowList` が存在します。
`Row k`から`RowList k`へは、いつでも `Prim.RowList`モジュールの型レベル関数 `RowToList`を使って変換することができます。

カインド`RowList k`を持つ型は、以下のいずれかの形で構成されます:
```
Nil :: forall k. RowList k 

Cons :: forall k. Symbol -> k -> RowList k -> RowList k
```
以上を用いて、たとえば与えられた行 `Row Type`から、その長さを計算して 型レベル整数として返すような型レベル関数を作ることができます:

```purs
import Prim.Int (class Add)
import Prim.Row as Row 
import Prim.RowList as RL

-- | Rowの長さを計算する型レベル関数
class RowLength :: Row Type -> Int -> Constraint
class RowLength row len | row -> len 

instance rowLength :: 
  ( RL.RowToList row rl　　　　　　-- 一旦RowListに変換して
  , RowListLength rl len         -- 補助関数を使ってRowListの長さを計算する 
  ) => RowLength row len

-- 補助関数
class RowListLength :: RL.RowList Type -> Int -> Constraint 
class RowListLength rl len | rl -> len

-- | Nilの長さは0
instance rlLengthNil ::
  RowListLength RL.Nil 0 

-- | Consの場合、(tailの長さ + 1) が求める長さになる
instance rlLengthCons ::
  ( RowListLength tail len -- tailの長さを再帰的に計算して
  , Add len 1 out          -- headの分を1加えて結果に束縛
  ) => RowListLength (RL.Cons k typ tail) out
```

`RowToList`を使って、一度rowをRowListに変換し、その後再帰的な関数でRowListの長さを計算していることに注目してください。
また、RowListLengthでは、RowListの型の形をNil, Consそれぞれの場合に対してインスタンス宣言を書いており、ちょうど値レベルのListを扱う関数におけるパターンマッチとの類似性がわかるかと思います。

**🗒️ 問題**
rowを受け取ると、rowに含まれるInt型のフィールドの数を計算する型レベルの関数 `CountInt` を作ってください。それに対応する値レベル関数も作ってください。

Hint: インスタンス宣言のConsのケースにおいて、headの型がIntのときと、そうでない場合を場合分けする。`else instance` をうまく使うこと。

<details><summary>解答</summary>

```purescript
class CountInt :: Row Type -> Int -> Constraint
class CountInt row len | row -> len 

instance rowLength :: 
  ( RL.RowToList row rl
  , CountIntRowList rl len
  ) => CountInt row len

class CountIntRowList :: RL.RowList Type -> Int -> Constraint 
class CountIntRowList rl len | rl -> len

instance rlLengthNil ::
  CountIntRowList RL.Nil 0 
  
instance countIntCons2 ::
  ( CountIntRowList tail len 
  , Add len 1 out 
  ) => CountIntRowList (RL.Cons k Int tail) out

else instance rlLengthCons ::
  ( CountIntRowList tail len 
  ) => CountIntRowList (RL.Cons k typ tail) len
```

</details>

# 値レベルプログラミングとの違い

型レベル関数と値レベル関数の大きな違いとして、Totalityについて言及しておきます。
たとえば、以下のような値レベルの関数

```purs
incr :: Int -> Int 
incr 0 = 1
incr 1 = 2
```

は、引数の値が0,1以外のときに返す値を定義していません。こういう関数を「Partialな関数」と言って、基本的にPureScriptはすべての関数に対してPartialでない（=Totalである）ことを要請するため、このような関数を書くとコンパイルエラーが出ます。

一方、型レベルの"関数"では、Totalityを強制することが**できません**。
そのため、以下のようなPartialな"型レベル関数"を普通に書くことができます（というか、Partialな関数しか書けない):

```
class PartialFunction a b | a -> b 

instance PartialFunction Int Boolean
instance PartialFunction Boolean String
```
これはIntに対してBooleanを、Booleanに対してStringを対応付ける"関数"です。
Int, Boolean以外の型に対しては戻り値を定義していないので、Partialな"関数"ということになります。
たとえば、この関数に入力としてCharを与えると（型レベル関数に対して引数を与える方法は後で述べます)、以下のようにエラーがでます:

```
  No type class instance was found for

    Main.PartialFunction Char
                         t1
```
これは、通常の値レベル関数における"Failed pattern match"の型レベル版だと思えばいいでしょう。

# よりよいエラー表示

型レベル計算をやっていて困るのが、**コンパイルエラー暗号になりがち問題**です。
実際、つい先程見たように、想定していない引数を受け取ったときのエラーメッセージが
`No type class instance was found for` っていうのは、型レベルプログラミングに慣れている人でも非常にわかりにくく、`InvalidArgument`みたいなイケてるエラーを出したいものです。

ご安心ください！PureScriptでは**プログラマが自由にカスタムのコンパイルエラーを作ることができる**ので、値レベルのプログラミングで好きなエラーメッセージと共に`throwError`するようなノリでエラーを発生させることが型レベルプログラミングでも可能です！

カスタムエラーを定義するには、`Prim.TypeError`モジュールをimportします。
このモジュールは、

 - カスタム型エラーのための型クラス `Fail`
 - カスタムエラーメッセージのカインド`Doc`
 - `Doc`カインドのデータ型コンストラクタ (`Text`, `Quote`, `Above`, `Beside`, etc)

を提供しています。

これを使って、たとえば型レベル除算関数で除数に０を指定したときにカスタムエラーを投げさせるようなことができます:

```
import Prim.TypeError (class Fail, Text, Quote)

-- 型レベル除算
class Div (a :: Int) (b :: Int) c | a b -> c 

instance zeroDivError :: 
  ( Fail (Text "Oh no! You cannot divide by zero!")
  ) => Div a 0 _undefined
```

長いメッセージは、 BesideとAboveを使ってDocとDocを結合することができ、
Besideは同じ行で結合し、Aboveは改行を挟んで結合します。
Docの中でなにか型を表示したい場合はQuoteが使えます。
実際は、BesideとAboveに適当な中置演算子のエイリアスを作ると可読性がよいでしょう。

```
infixl 6 type Beside as ++
infixl 5 type Above as |>

type LongMsg = Text "This is long doc!"
  |> Text "And this line has quoted type: " ++ Quote Int
  |> Text "I'm more loooooooooooong"
  |> Text "日本語もイケるぜ！（控えたほうがいいけどね)"

f :: Fail LongMsg => Unit 
f = unit

main :: Unit
main = f
```
これをコンパイルすると以下のエラーが出ます:
```
  Custom error:

    This is long doc!
    And this line has quoted type: Int
    I'm more loooooooooooong
    日本語もイケるぜ！（控えたほうがいいけどね)

while checking that type Fail (Above (Above (Text "This is long doc!") (Beside ... ...)) (Text "I\'m more loooooooooooong")) => Unit
  is at least as general as type Unit
while checking that expression f
  has type Unit
in value declaration main```
```
Note: 
`Fail`, `Doc`は、値レベルプログラミングにおける`throw`, `Error`の型レベル版と見ることができ、このモジュール自体が一種の型レベルプログラミングの例になっていますね。

# ユーザー定義カインド

ここまで見てきたように、PureScriptはPrimとPreludeだけでも豊富な型レベルプログラミングの道具が提供されており、これだけでも結構なことができるのですが、時には概念をより正確に表現するための**独自のデータ型が作りたくなる**ものです。

型レベルプログラミングでも同様に、**独自にカインドを作って、そのカインドを持つ型を使ってプログラミングする**ことができます。

PureScriptでは、コンストラクタのないデータ型を宣言することでカスタムのカインドを定義し、`foreign import data`構文でそのカインドを持つ型を定義することができます。
以下はこのイディオムをつかって、型レベルMaybeを作る例です：

```purs
data Maybe k
foreign import data Nothing :: forall k. Maybe k 
foreign import data Just :: forall k. k -> Maybe k
```

型レベル関数（つまり型クラス）の宣言では、次のようにカインドアノテーションを明示することができるので、
これにより（多少は）型レベルプログラミングでも型付け言語のような感覚でコーディングができます:
```
-- Data.MaybeのfromMaybeの型レベル版。

class FromMaybe :: forall k. Maybe k -> k -> k -> Constraint 
class FromMaybe m def out | m def -> out 

instance fromMaybeNothing :: FromMaybe Nothing def def
instance fromMaybeJust :: FromMaybe (Just a) _1 a
```

**🗒️ 問題** 
先ほど作った`GetAt`は、Partialな関数になっており、`row`に指定されたラベルの要素がなければエラーになってしまいます。そこで、`Maybe`カインドを使って、要素がなければ`Nothing`を返すように改良したいです。
作るべきものは、以下のシグネチャを持つ型レベル関数です:

```purs
class GetAt :: forall k. Symbol -> Row k -> Maybe k -> Constraint 
class GetAt s row out | s row -> out 
```

 1. このような`GetAt`を実装してください。 `RowToList`を用いて一旦`row`を`RowList k`に変換し、再帰的に`s`を探す補助関数を用いてください

 2. RowListを使わずに、以下のように実装するとうまく動きません。なぜでしょうか？
    ```purs
    import Prim.Row as Row

    instance getAtJust ::
      ( Row.Cons k typ rest row 
      ) => GetAt row k (Just typ)
    else instance getAtNothing :: GetAt row k Nothing
    ```

# 型レベル関数の呼び出し

ここまで、色々と型レベルの関数を書いてきましたが、呼び出し方について説明していませんでした。
ここでは、型レベル関数を呼び出して、コンパイル時に型の計算をさせる方法を説明します。

これには値レベルと型レベルの２つの世界を橋渡しするための型である `Proxy` を用います。
Proxyは、`Type.Proxy`モジュールで以下のように定義されています:

```
data Proxy :: forall k. k -> Type
data Proxy t = Proxy
```

たとえば、`GetAt`関数を使うために、以下のように`GetAt`を制約にもつ関数を作り、
型レベル関数の引数(`s`と`row`）を、Proxy経由で受け取るようにします:
```
import Type.Proxy (Proxy(..))

getAt 
  :: forall s row out
   . GetAt s row out 
  => Proxy s
  -> Proxy row 
  -> Proxy out
getAt _ _ = Proxy
```

この関数を、以下のように呼び出すことで、行`( foo :: Int, bar :: Boolean )`からフィールド`foo`を取得する型レベル計算をコンパイラに行わせることができます:

```
  let 
    _ = getAt (Proxy :: _ "foo") (Proxy :: _ (foo :: Int, bar :: Boolean))
  in
    ...
```

ちなみに、最近のコンパイラでは **Visible Type Application**がサポートされ、これを用いればProxyを用いずにダイレクトに型レベル計算に型を渡すような書き方でコーディングができます:

```
getAt 
  :: forall @s @row out   -- s, rowはVisible Type Application可能
   . GetAt s row out 
  => Proxy out
getAt = Proxy

-- 呼び出す側はType Applicationで呼び出す
f = 
  let 
    _ = getAt @"foo" @(foo :: Int, bar :: Boolean)
  in 
    ...
```
# 具体例：単純型付きラムダ計算

それでは、以上に述べてきたツールを使って、実際にnon-trivalな規模の型レベルアプリケーションを作ってみましょう！
題材としては、 **単純型付きラムダ計算(Simply Typed Lambda Calculus)** の型検査器をPureScriptの型システムで実装してみます。

ラムダ計算とは、関数（抽象)と適用だけを持ったすこぶるシンプルな計算体系で、以下のようなシンタックスを持つ一風変わった関数型言語だと思ってもらえればよいです

```
変数 v
関数 λx. t  ... purescript風に書くと \x -> t
適用 t1 t2  ... purescript風に書いても t1 t2
```

単純型付きラムダ計算は、ラムダ計算に**単純型**を導入して拡張したものです。
単純型とは、以下のように**アトム型** (`Nat`とか`Bool`みたいにアプリオリに定義された型)と、
２つの型`T1`, `T2`で作る関数型 `T1 -> T2`だけからなるとします。
STLCの文法は、以下に要約されます:

```
T                ; Types
  ::= A          ; Atom types
      T1 -> T2   ; Function types

t                ; Terms 
  ::= x          ; Variables
      λx:T.t     ; Abstraction
      t1 t2      ; Application
```

STLCにおける型検査は、**型付け文脈(Typing Context)**・項・型という３つのエンティティの関係により記述されます。

型付け文脈とは、型判定を行う対象の項のスコープにおいて定義済みの変数とその型の組のリストで、`Γ`という記号で書かれることが多いです。

型文脈`Γ`において、項 `t` が型 `T` を持つとき、これを以下のように書きます
```
Γ ⊢ t : T
```
STLCにおける型付け規則を以下に列挙します。

- **Variable rule**　（T-VAR)
```
(x:T) ∈ Γ
----------
Γ ⊢ x : T
```
- **Application rule** (T-APP)
```
Γ ⊢ t1 : T1 -> T
Γ ⊢ t2 : T1
-----------------
Γ ⊢ t1 t2 : T
```

- **Abstraction Rule** (T-ABS) 

```
Γ, (x:T1) ⊢ t : T2
---------------------
Γ ⊢ λx:T.t : T1 -> T2
```

型付け規則は、「横棒の上のステートメントがすべて成り立つ時、横棒の下のステートメントが言える」と読んでください。
たとえば、Abstraction ruleは、「現在のコンテキスト`Γ`に変数`(x:T1)`が追加されたコンテキストにおいて項`t`が型`T2`を持つとき、抽象`λx:T.t`は関数型`T1 -> T2`を持つ」という主張です。


ここでは、「`Γ`と`t`が与えられたときに`T`を出力する（計算できない時は型エラーとしてレポートする）」という問題を、PureScriptの型システムで実装したいと思います。

## STLCのシンタックスを型で表現する

まず、STLCにおける型を実装します。
前述したように、型レベル計算を行う場合、PureScriptの既存の型にのっかる場合と、ユーザ定義カインドを用意する２つのアプローチがあります。
ここでは後者のアプローチをとります。

```purs
data Type_

foreign import data TAtom :: Symbol -> Type_ 
foreign import data TFunc :: Type_ -> Type_ -> Type_ 

-- E.g.
type Nat = TAtom "Nat"
type Bool = TAtom "Bool"
type Nat2Bool = TFunc Nat Bool     -- Nat → Bool
```

次に項を型で表現します。

```purs
-- 変数名は型レベル文字列で
type Var = Symbol

data Term

foreign import data TmVar :: Var -> Term 
foreign import data TmAbs :: Var -> Type_ -> Term -> Term
foreign import data TmApp :: Term -> Term -> Term

-- e.g.
type IdNat = TmAbs "x" Nat (TmVar "x")   -- λ(x:Nat).x 
```

これで、STLCにおける有効な項がPureScriptの型で表現できるようになりました。

我々の課題は、カインド`Term`の型からカインド `Type_` の型を計算することです。
これはもちろん`Term -> Type_`なる型レベルの関数ですから、型クラスのfundepで表現します!
型文脈は、シンプルにPureScriptのRowListを使いましょ。

```
import Type.RowList as RL

type TypeContext = RL.RowList Type_ 

-- ContextとTerm から Type を計算するので、このシグネチャになる
class InferType (ctx :: TypeContext) (tm :: Term) (typ :: Type_) | ctx tm -> typ
```

上で挙げた３つの型付け規則に対応する形で、`InferType`"関数"の本体、すなわち型クラスのインスタンスを実装していきます。

## エラーハンドリング

その前に、これらの３つのルールがどれも当てはまらない場合、型検査器は型エラーをレポートすることになります。
我々のSTLCの場合、以下の３つのエラーが発生する可能性があります:
  - コンテキストに定義されていない変数が使われている
  - 関数に引数の型と異なる項が与えられている
  - 関数でない項に対して関数適用が行われている

これらのうち最後の２つは、ともに「型が一致しない」というエラーにまとめられますから、以下のように２つの型エラーを作っておきます:

```
data TypeError 
foreign import data UnboundVariable :: Var -> TypeError           -- 変数が定義されていない
foreign import data TypeMismatch :: Type_ -> Type_ -> TypeError   -- 型が一致しない
```
そして、これらのTypeErrorを投げて型検査を終了させるための型レベル関数を、以下のように作っておきます:

```
class FailWith :: TypeError -> Constraint
class FailWith err
```

## 型付規則の実装
このようにエラーハンドリングを準備した上で、まずはVariable rule (T-VAR) から始めます。
```
(x:T) ∈ Γ
----------
Γ ⊢ x : T
```
これを実装するには型文脈を参照して指定された変数に対する型を求める関数が必要です。
これは`TypeContext`と`Var`から`Type_`を計算する"関数"ですから、以下のシグネチャになりますね:
```purs
class SearchVar (ctx :: TypeContext) (var :: Symbol) (typ :: Type_) | ctx var -> typ
```

この関数の実装は、

- コンテキストにエントリがあるなら、その変数名がターゲットの変数名と比較し、
   - 一致していればその型を返す
   - 違っていればコンテキストの残りに対して検索を続ける
- 空コンテキストに到達すると、コンテキストに定義されていない変数となるため、エラー

とすればよいわけですから、以下のようになります:
```purs
-- TypeContextがNilなら、変数がコンテキストで宣言されていないためエラー
instance searchVarNil ::
  ( FailWith (UnboundVariable var)
  ) => SearchVar RL.Nil var _2

-- TypeContextの先頭の変数名がターゲットの変数名と同じなら、その型を返す
else instance searchVarFound :: SearchVar (RL.Cons var typ _1) var typ

-- 上記以外なら、TypeContextのtailについて再帰的に検索を続ける
else instance searchVarNext ::
  ( SearchVar tail var typ
  ) => SearchVar (RL.Cons _1 _2 tail) var typ 
```

これを用いて、T-VAR ruleは以下のように実装されます:
```purs
-- T-VAR
instance 
  ( SearchVar tctx var typ
  ) => InferType tctx (TmVar var) typ
```

続いて、T-ABSです。
```
Γ, (x:T1) ⊢ t : T2
---------------------
Γ ⊢ λx:T.t : T1 -> T2
```

λ抽象の引数`x`とその型`T1`でextendしたコンテキストにおいて、抽象の本体`t`の型を計算するわけですから、以下のようになります:
```
else instance inferTypeAbs ::
  ( InferType (Cons x t1 tctx) body t2 
  ) => InferType tctx (TmAbs x t1 body) (TFunc t1 t2) 
```
型コンテキストは`RowList Type_`で表現しているので、新しい変数による拡張は単純にRowListとしてConsすればよいことに注意してください。
※相変わらずshadowingは考慮していないです。

最後にT-APPです。これは少しややこしいです。

```
Γ ⊢ t1 : T1 -> T
Γ ⊢ t2 : T1
-----------------
Γ ⊢ t1 t2 : T
```

まず、関数項`t1`と引数項`t2`の型をそれぞれ計算し、そのあと
- 関数項の型が正しく関数型になっている
- かつ、その引数の型`T1`が引数項の型とマッチしている
ことを確認せねばなりません。

まず、引数型がマッチしていることの確認を、以下のように補助関数に切り出しましょう。
```purs
class TypeCheckApp typ1 typ2 typ | typ1 typ2 -> typ 

-- typ1が関数型で、その引数の型がtyp2と一致していればOK
instance typecheckAppOK :: TypeCheckApp (TFunc t1 t2) t1 t2

-- typ1が関数型でも、引数の型(t1)とtyp2が一致しなければOUT
else instance typecheckAppMismatch1 :: 
  ( FailWith (TypeMismatch t1 t3)
  ) => TypeCheckApp (TFunc t1 t2) t3 _1

-- typ1が関数型じゃなければOUT
else instance typecheckAppMismatch2 ::
  ( FailWith (TypeMismatch (TFunc t2 (TVar "?")) t1)
  ) => TypeCheckApp t1 t2 _1
```

これを用いて、T-Appを以下のように実装できます：
```purs
else instance interTypeApp ::
  ( InferType tctx tm1 typ1
  , InferType tctx tm2 typ2
  , TypeCheckApp tm1 tm2 typ  
  ) => InferType tctx (TmApp tm1 tm2) typ
```

## 完成！

以上で、型検査のための関数が完成しました！
改めて完全なコードを載せておきます:

<details><summary>STLC 完全なコード</summary>

```
module STLC where

import Prim.Symbol (class Append)
import Prim.TypeError (class Fail, Doc, Text, Beside, Above)
import Type.Equality (class TypeEquals)
import Type.RowList as RL

--
-- Syntax of STLC
-- 

-- | Variable are represented as Symbol (a.k.a. Type-level String)
type Var = Symbol

-- | Types in STLC
data Type_
foreign import data TAtom :: Var -> Type_ 
foreign import data TFunc :: Type_ -> Type_ -> Type_ 

-- | Terms in STLC
data Term
foreign import data TmVar :: Var -> Term 
foreign import data TmAbs :: Var -> Type_ -> Term -> Term
foreign import data TmApp :: Term -> Term -> Term


-- | Typing context
type TypeContext = RL.RowList Type_ 

--
-- Semantics of STLC
--

class SearchVar :: TypeContext -> Var -> Type_ -> Constraint
class SearchVar tctx var typ | tctx var -> typ

instance searchVarNil ::
  ( FailWith (UnboundVariable var)
  ) => SearchVar RL.Nil var _2

else instance searchVarFound :: SearchVar (RL.Cons var typ _1) var typ

else instance searchVarNext ::
  ( SearchVar tail var typ
  ) => SearchVar (RL.Cons _1 _2 tail) var typ 

-- | Type-checking
class InferType :: TypeContext -> Term -> Type_ -> Constraint
class InferType tctx tm typ | tctx tm -> typ

instance 
  ( SearchVar tctx var typ
  ) => InferType tctx (TmVar var) typ

else instance inferTypeAbs ::
  ( InferType (RL.Cons x t1 tctx) body t2 
  ) => InferType tctx (TmAbs x t1 body) (TFunc t1 t2) 

else instance interTypeApp ::
  ( InferType tctx tm1 typ1
  , InferType tctx tm2 typ2
  , TypeCheckApp typ1 typ2 typ  
  ) => InferType tctx (TmApp tm1 tm2) typ

-- | A helper function for checking application 
class TypeCheckApp :: Type_ -> Type_ -> Type_ -> Constraint
class TypeCheckApp typ1 typ2 typ | typ1 typ2 -> typ 

instance typecheckAppOK :: TypeCheckApp (TFunc t1 t2) t1 t2

else instance typecheckAppMismatch1 :: 
  ( FailWith (TypeMismatch t1 t3)
  ) => TypeCheckApp (TFunc t1 t2) t3 _1

else instance typecheckAppMismatch2 ::
  ( FailWith (TypeMismatch (TFunc t2 (TAtom "?")) t1)
  ) => TypeCheckApp t1 t2 _1

-- 
-- Pretty-printing errors
--

class PrettyPrint :: forall k. k -> Symbol -> Constraint
class PrettyPrint a s | a -> s 

instance ppTAtom ::
  PrettyPrint (TAtom t) t
instance ppTFunc ::
  ( PrettyPrint typ1 pp1
  , PrettyPrint typ2 pp2
  , Append "(" pp1 ppt1
  , Append ppt1 " -> " ppt2
  , Append ppt2 pp2 ppt3
  , Append ppt3 ")" ppt
  ) => PrettyPrint (TFunc typ1 typ2) ppt

infixl 6 type Beside as ++
infixl 5 type Above as |>

-- | types of type-checking errors
data TypeError 
foreign import data UnboundVariable :: Var -> TypeError
foreign import data TypeMismatch :: Type_ -> Type_ -> TypeError

-- | Pretty printing error 
class Describe :: TypeError -> Doc -> Constraint
class Describe err doc | err -> doc

instance descUnboundVariable :: 
  Describe 
    (UnboundVariable var) 
    (Text "Unbound variable: " ++ Text var)

instance descTypeMismatch ::
  ( PrettyPrint typ1 pt1
  , PrettyPrint typ2 pt2
  , TypeEquals msg 
    ( Text "Types do not match:"
    |> Text " - Expect: " ++ Text pt1
    |> Text " - Found: " ++ Text pt2
    )
  ) => Describe (TypeMismatch typ1 typ2) msg
  
class FailWith :: TypeError -> Constraint
class FailWith err

instance failwithTypeError ::
  ( Describe err msg
  , Fail msg
  ) => FailWith err
```
</details>

これを用いて、簡単な型検査をやってみますと...

```
-- λ(f: Nat -> Bool). λ(x: Nat). f x 
type Test = TmAbs "f" (TFunc (TAtom "Nat") (TAtom "Bool")) 
  (TmAbs "x" (TAtom "Nat") 
    (TmApp (TmVar "f") (TmVar "x"))
  )

infer :: forall @tm typ. InferType RL.Nil tm typ => Proxy typ
infer = Proxy 

test :: Proxy ?x 
test = infer @(Test)
```
以下のようにキチンと推論されました🎉
```
  Hole 'x' has the inferred type

    TFunc (TFunc (TAtom "Nat") (TAtom "Bool")) (TFunc (TAtom "Nat") (TAtom "Bool"))


in value declaration test
```

しかしこのようにNatとBoolを間違えてしまうと...
```
-- λ(f: Nat -> Bool). λ(x: Bool). f x 
type Test = TmAbs "f" (TFunc (TAtom "Nat") (TAtom "Bool")) 
  (TmAbs "x" (TAtom "Bool") 
    (TmApp (TmVar "f") (TmVar "x"))
  )
```

しっかりと型エラーが出ます！！ 🎉🎉🎉

```
  Custom error:

    Types do not match:
     - Expect: Nat
     - Found: Bool
```

# まとめ

ということで、本記事ではPureScriptにおける型レベルプログラミングについて解説を行いました！
このテーマの記事で一番くわしい入門者向けの解説を目指した結果、なかなかの分量になってしまいました😅
最初に述べた通り、型レベルプログラミングは値レベルのプログラミングと大した差はないんだな、ということがわかっていただければ幸いです。

なお、今回の記事で書いた型レベル関数は、すべてメンバーを持たないクラスになっていますが、
実際には型クラスにメンバーをもたせ、値レベルの関数と型レベル関数をセットで書くほうが実用上は多いです。
それについては、もしかしたら続編という形で改めて記事に書くかもしれませんが、型レベル計算に基づく良質なライブラリの実装を参照されると大変勉強になるかと思います。
PreludeのRecord周りのモジュールも大変参考になります。

参考として、以下のようなライブラリを挙げておきます:
  - [purescript-fmt](https://github.com/m-bock/purescript-fmt)  ... Printfのようなフォーマッティングのためのライブラリ
  - [purescript-record-studio](https://github.com/rowtype-yoga/purescript-record-studio) ... 型レベル計算による、レコードメタプログラミングのライブラリ