【翻訳】型クラスとインスタンス宣言は、型レベルのパターンマッチです！

この記事は Type classes and instances are pattern matching for types by @kimagure の翻訳版です。

purescriptで型レベルプログラミングを覚えたいと考えていた時、元記事を見つけて「インスタンス宣言はパターンマッチ」という視点がとても理解の助けになりました。日本語検索でも引っかかるようになるといいなと思ったので、この翻訳版を作らさせてもらいました。以下から本文です↓

---

最近、ニューヨークの超高層ビル10 Hudson YardsにてNY PureScriptの交流会があり、そこで話をする機会がありました。
そのとき、関数従属とインスタンス型引数がどのように機能するかについて、いくつか質問がありました。関数従属によってどの型がマッチするのかしないのか。インスタンス型引数とcase式はどのように似ているのか。
それは1対1の関係とは言えませんが、階層がひとつ違うだけで同じ概念がたくさんあります。型レベルプログラミングは魔法か何かではないので、私はこのことについて書く価値があると思いました。

例題 （型安全にレコードをリストに変換）

ではさっそく、逐次処理のための RowList、入力レコードの #Type、 Type を型引数にとる型クラスを定義してみましょう。Type（a）は入力レコードが同質であることを保証するために使います。

class Values (xs :: RL.RowList) (row :: # Type) a
  | xs -> row a
  where
    values :: RLProxy xs -> { | row } -> L.List a

関数従属 xs -> row a はインスタンスのマッチングに使われる記述です。この場合 xs :: RowList だけがインスタンスのマッチングに使われることになります。

Nil

ところで、この型クラスの Nil インスタンスはどう書けば良いでしょうか？普通はインスタンス型引数 row に具体的な型 () を直接与えます。

instance nilValues ::
  Values RL.Nil () a where
  values _ _ = L.Nil

しかし、ここでの () はインスタンスのマッチングに使われません。したがって代わりに次のような制約を与えても同じことです。

instance nilValues ::
  ( Eq.TypeEquals { | row } {}
  ) => Values RL.Nil row a where
  values _ _ = L.Nil

それか、TypeEqualsのレコード版を定義して使っても良いです。

class Eq.TypeEquals {|r1} {|r2}
   <= RowEquals (r1 :: # Type) (r2 :: # Type)

このように型クラス Values の Nil インスタンスだけ定義することは、値レベルにおいて部分関数を定義することに似ています。

matchEmpty :: Partial => L.List Int -> M.Map String Int -> Boolean
matchEmpty xs r = case xs, r of
  L.Nil, empty' ->
    false
  where
    empty' = M.empty

（このままではempty'は使われないので、）guardを使うと次のように書けます。

matchEmpty :: Partial => L.List Int -> M.Map String Int -> Boolean
matchEmpty xs r = case xs, r of
  L.Nil, r' | r' == empty' ->
    false
  where
    empty' = M.empty

これは分かりやすいと思います。インスタンス宣言で型引数に制約を与えることは、case式のguardとよく似ています。
違いは、guardはcase式に追加の条件を続けて使える一方、インスタンス制約は破綻しているとコンパイル時のエラーになります。（インスタンスチェーンとの関連もありますが、今は重要でないので省略します）
このアナロジーを用いれば、もしインスタンスを正しくマッチングできるのならば、型クラスは部分関数の型版にすぎません。コンパイル時に評価されてビルドに成功する部分関数です。しかし実際のcase式は Partial を作ることもできます。それが原因でプログラムが実行時に落ちることは最悪の事態です。
PureScriptユーザーとしては、このような部分関数をコンパイル時に問題なく扱えることを心から望みます。特定の場合にエラーを表示するための Error 制約さえあり、不安全にコンパイルを落とします。

Cons

続いて、レコードの値を取得する Cons インスタンスは次のように書けます。

instance consValues ::
  ( IsSymbol name
  , Values tail row' a
  , R.Cons name a row' row
  , R.Lacks name row'
  ) => Values (RL.Cons name a tail) row a where
  values _ r = L.Cons first rest
    where
      nameP = SProxy :: SProxy name
      first = Record.get nameP r
      r' = Record.delete nameP r :: { | row' }
      rest = values (RLProxy :: RLProxy tail) r'

前と同じように、Consの型引数に制約を与えることもできます。

instance consValues ::
  ( IsSymbol name
  , Values tail row' a
  , Eq.TypeEquals a ty
  , R.Cons name ty row' row
  , R.Lacks name row'
  ) => Values (RL.Cons name ty tail) row a where
  values _ r = L.Cons first rest
    where
      nameP = SProxy :: SProxy name
      --- インスタンス型引数がマッチしない場合は、equalityを適用する必要があります
      first = Eq.from $ Record.get nameP r
      r' = Record.delete nameP r :: { | row' }
      rest = values (RLProxy :: RLProxy tail) r'

ここでは TypeEquals a ty を使っているので、from を使ってレコードの ty 型の値を List a のために変換しななければなりません。

このように Cons インスタンスを定義することは、値レベルにおいてguardを値に適用することに相当します。たとえば、1 の値しか取らない List Int は次のようになるでしょう。

addOnesPartial :: Partial => Int -> L.List Int -> Int
addOnesPartial acc xs = case xs of
  L.Cons x tail
    | x == 1
    -> addOnesPartial (x + acc) tail

  -- それか、インスタンス型引数のように直接値でマッチングします
  -- L.Cons 1 tail
  --   -> addOnesPartial (1 + acc) tail

  L.Nil -> acc

しかし前と同様に、これは実行時に扱うのは悲惨です。事前にバリデーションするか、フィルタした方が良いです。

addOnes :: Int -> L.List Int -> Int
addOnes acc xs = case xs of
  L.Cons x tail
    | x == 1
    -> addOnes (x + acc) tail
  L.Cons x tail
    -> addOnes acc tail
  L.Nil -> acc

これらの例を実行！

addOnesPartial をいくつか実行してみましょう。

  -- 1
  log $ show $ unsafePartial $ addOnesPartial 0 (L.Cons 1 L.Nil)

  -- partialityによって落ちます。
  -- log $ show $ unsafePartial $ addOnesPartial 0 (L.Cons 2 L.Nil)

予想通り、1 を与えた場合のみ動作する部分関数を定義したので、2 を与えた場合は落ちます。 Partial を関数に使う場合、落ちても驚くことはありません。

次に、レコードの値の使い方を見てみましょう。最初にヘルパ関数を定義します。

values'
  :: forall xs row a
   . RL.RowToList row xs
  => Values xs row a
  => { | row }
  -> L.List a
values' = values (RLProxy :: RLProxy xs)

これは、Values に伴って生成される RowList によって、具体的に型づけされたレコードなら何でも動作します。例を見ましょう。

main = do
  -- (1 : 2 : Nil)
  log $ show $ values' {x: 1, y: 2}

レコードが同質であるように定義したので、これは予想通り動きます。一方そうでないレコードを与えるとどうなるでしょうか？

  -- コンパイルエラー: Int型がString型にマッチしません
  log $ show $ values' {x: "A", y: 2}

この場合、コンパイル時のエラーは次のようになります。

  Could not match type

    Int -- Int型に遭遇しました

  with type

    String -- String型を予想していたのに


while solving type class constraint

  Main.Values (Cons "y" Int Nil) -- RowListのフィールド
              t3 -- 推論される何かの型
              String -- String型がインスタンス制約の型でした

while applying a function values' -- 定義した関数と推論された型
  of type RowToList t0 t1 => Values t1 t0 t2 => { | t0 } -> List t2
  to argument { x: "A" -- 与えた値
              , y: 2
              }
while inferring the type of values' { x: "A"
                                    , y: 2
                                    }
in value declaration main

じっくりエラーを読むならば、実はかなり多くのことを知らなければなりません。もちろん、エラーに遭遇したら、インスタンス型引数とその制約を確認しないと少し困惑します。しかしそれは、もっとドキュメント追加するか、より明確なエラーを提供する今後のインスタンスチェーンによって解決できるでしょう。

※ インスタンスチェーンは使えるようになりました。
Instance Chains - Type Classes

結論

型クラスのインスタンスマッチングとcase式の間には、実に多くの共通点があることを説明できたと思います。この記事を読んだ後には、型クラスで RowList のを使う際の Nil と Coos、case式で List a を使う際の Nil と Cons の関連がよりクリアになっていることを願います。

型レベルのレコード

kind	RowList
data	Nil :: RowList
data	Cons :: Symbol -> Type -> RowList -> RowList

値レベルのリスト

data	List a
value	Nil :: List a
value	Cons :: a -> List a -> List a

参考リンク

• This repo: https://github.com/justinwoo/fundeps-instances-sum-case-guards-demo
• https://leanpub.com/purescript/read#leanpub-auto-type-classes
• https://leanpub.com/purescript/read#leanpub-auto-functional-dependencies

---

※ 翻訳以外に下記について手を加えています。

• 現在のPureScriptのバージョンv0.13で動くようにコードを微修正
• モジュールにエイリアス名をつけて参照しやすいように修正
• 本文中のいくつかの箇所を少し補足

※ 記事中のコードで使われているモジュールのエイリアス名

import Data.List as L
import Data.Map as M
import Prim.Row as R
import Prim.RowList as RL
import Record as Record
import Type.Equality as Eq