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

この記事は、PureScript Advent Calendar 2024 の 5日目の投稿です。

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

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

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

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

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

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

このような事情は以下のように図示できます:

型                \ コンパイル時
↓ 分類             |
↓　　　　　　     　/
値 ------> 値     \ 実行時
    関 数         |
                 /

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

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

これが、先程の値レベルプログラミミングの図と同じよう形をしていることに注目してください。
型レベルは

• 値 => 型
• 型 => カインド
• 関数 => 「型レベル関数」

と、レベルを１つシフトさせ、それぞれのレベルの登場人物をうまく対応付けてやれば、
型レベルプログラムも値レベルのプログラムとほぼ同様に捉えることができるのです。
こう考えれば、一見すると闇の呪文のような型レベルプログラムも、普通に読み書きができるようになるはずです。

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

型レベルの"関数"

それでは、型レベルの関数とはなんでしょうか？
通常の値レベルプログラミングで考えると、関数とは値に対して値を対応させるものです:

incr :: Int -> Int 
incr x = x + 1      -- Intの値xに対して、x + 1という値を対応付ける

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

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

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

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のインスタンスになっているので:

instance MonadThrow Error Effect where ...

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

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 を戻り値とする

この型レベル関数は、以下の値レベル関数に対応しています：

greet :: String -> String
greet name =
  let 
    out1 = "Hello, " <> name
    out = out1 <> "!"
  in 
    out

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

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に対応する値レベルの関数を書いてください。

解答

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'

RowとRowList

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

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

Row Typeは、「順序を持ったラベル付き型の配列」のような型で、たとえば以下のような型がRow Typeカインドに属します:

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から、その長さを計算して 型レベル整数として返すような型レベル関数を作ることができます:

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 をうまく使うこと。

解答

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

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

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

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を作る例です：

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を返すように改良したいです。
作るべきものは、以下のシグネチャを持つ型レベル関数です:

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を使わずに、以下のように実装するとうまく動きません。なぜでしょうか？

   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の既存の型にのっかる場合と、ユーザ定義カインドを用意する２つのアプローチがあります。
ここでは後者のアプローチをとります。

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

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

-- 変数名は型レベル文字列で
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_を計算する"関数"ですから、以下のシグネチャになりますね:

class SearchVar (ctx :: TypeContext) (var :: Symbol) (typ :: Type_) | ctx var -> typ

この関数の実装は、

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

とすればよいわけですから、以下のようになります:

-- 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は以下のように実装されます:

-- 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が引数項の型とマッチしている
  ことを確認せねばなりません。

まず、引数型がマッチしていることの確認を、以下のように補助関数に切り出しましょう。

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を以下のように実装できます：

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

完成！

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

STLC 完全なコード

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

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

-- λ(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 ... Printfのようなフォーマッティングのためのライブラリ
• purescript-record-studio ... 型レベル計算による、レコードメタプログラミングのライブラリ