このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

ほぼワケワカラン疑似コード

とある論文で、説明のためにHaskell風疑似コードが使われていました。そのひとつが次:

data 0 a

instance Functor 0 where
  fmap =

ウーム、わかる人にはわかるのかも知れないけど、ほぼ意味不明。いったい何を言いたいのでしょう? 僕が説明します。$`\newcommand{\Imp}{\Rightarrow }
\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\In}{\text{ in } }
\newcommand{\id}{\mathrm{id} }
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } }%
\newcommand{\Where}{\Keyword{Where } }%
\newcommand{\Define}{\Keyword{Define } }%
`$

内容:

単元集合型と空集合型

冒頭に挙げた疑似コードでは、'0' が数字一文字からなる名前〈識別子〉として使われています。通常、数字からはじまる文字列は名前に使えないので、次のように書き換えましょう。

data Zero a

instance Functor Zero where
  fmap =

最初の行 data Zero a の説明は、曰く「void型を作る型構成子〈type constructor〉だ」と。文脈から言って、void型は空集合の型のようです。

まず言葉づかいとして、伝統的に「void型」は単元集合〈singleton set〉の型を意味します。ユニット型、シングルトン型とも呼びます。空集合の型は、never型とかnothing型とか呼ぶようです。空集合の型を型システムに明示的に導入するようになったのは最近のことです(古いプログラミング言語だと、空集合の型は持ってない)。

辞書を引くと、void は確かに empty と同義なので、「void型 = empty型 = 空集合型」と誤解する、あるいはそういう意味で使いたい気持ちはわかりますが、混乱を避けるために次の約束を守ったほうがいいでしょう。

  • 単元集合の型 = void型
  • 空集合の型 = never型

例えば、プログラムにおける関数の戻り値の型がvoid型なら、それは決まり切った単一の値を返して正常終了します。しかし、関数の戻り値の型がnever型なら、その関数は正常終了することはなく、無限走行するか例外を投げます。

言葉の話はこれくらいにして、data Zero a が定義する関数をラムダ式で定義してみましょう。

$`\Define \mrm{Zero} :=
\lambda\, a\in {\bf Type}.(\, \emptyset\;\in {\bf Type}\,)
%`$

$`\mrm{Zero}`$ は、$`{\bf Type}`$ から $`{\bf Type}`$ への関数〈写像〉で、常に値 $`\emptyset`$ をとる“定数関数”です。$`\emptyset`$ は空集合ですね。

しかしところで、$`{\bf Type}`$ って何でしょう?

型の集合と型構成子

$`{\bf Type}`$ について説明します。

圏 $`\cat{C}`$ を、集合圏 $`{\bf Set}`$ の部分圏だとします。次は成立します。

$`\quad a\in |\cat{C}| \Imp a\in |{\bf Set}| \Iff (a \text{ は集合})`$

サイズの大きな集合を扱いたくないので、$`\cat{C}`$ は小さい圏だとします。つまり、次を要求します。

$`\quad |\cat{C}| \in |{\bf Set}|`$

もしサイズの問題が気にならないなら、上の条件は不要です。

さらに、$`\cat{C}`$ はデカルト閉圏だとして、そのデカルト積〈直積〉と指数は $`\times,\, [-,-]`$ で表します。$`[a, b] = \cat{C}(a, b)`$ を仮定します。$`\emptyset \in |\cat{C}|`$ も仮定します*1

以上のような圏 $`\cat{C}`$ をひとつ選んで固定します。固定した $`\cat{C}`$ に対して次のように定義します。

$`\Define {\bf Type} := |\cat{C}|`$

集合 $`{\bf Type}`$ は圏 $`\cat{C}`$ に対して相対的に決まりますが、$`\cat{C}`$ を固定した後は固有特定の集合なので、太字(固有名詞の書き方)としました。

集合 $`{\bf Type}`$ の要素(要素も集合)を〈type〉と呼びます。もちろんこの呼び名は Sets-as-Types の立場でのことで、他の Xxx-as-Types の立場なら「型」の定義も変わります*2

デカルト積と指数 $`\times,\, [-,-]`$ は、圏 $`\cat{C}`$ 上の二項関手〈双関手〉(指数は反変・共変の二項関手)ですが、対象の集合である $`{\bf Type}`$ に制限すれば、次のような写像になります。

$`\quad (- \times -) : {\bf Types}\times {\bf Type} \to {\bf Type}\\
\quad [-, -] : {\bf Type}\times {\bf Type} \to {\bf Type}
%`$

一般に、$`{\bf Type}^n \to {\bf Type}`$ の形の写像を型構成子〈type constructor〉といいます。特に、$`n = 0`$ のときの型構成子 $`T`$ は:

$`\quad T:{\bf Type}^0 = {\bf 1} \to {\bf Type}`$

$`{\bf 1}`$ は単元集合なので、$`T`$ は単一の型〈集合〉をポイントします。単一の型も型構成子の特殊なものとみなせます。言い方を変えれば、型構成子は型の一般化です。なので、言葉の拡大解釈として、型構成子を「型」と呼んでしまうこともあります。

n項の〈n引数の〉型構成子の全体を次のように書きましょう。

$`\For n \in {\bf N}\\
\Define {\bf TypeCons}_n := \mrm{Map}({\bf Type}^n, {\bf Type}) = {\bf Set}({\bf Type}^n, {\bf Type})`$

0項の型構成子は型と同一視できることは次のように書けます。

$`\quad {\bf TypeCons}_0 \cong {\bf Type}`$

型構成子を関手に拡張

前節の説明で、写像 $`\mrm{Zero}:{\bf Type} \to {\bf Type}`$ の意味はハッキリしました。「ハッキリした」とは、写像の域・余域である $`{\bf Type}`$ の正体がわかり、写像の正体も(定数関数として)よくわかった、ということです。そして、ハッキリしてないことを「ワケワカラン」とか「意味不明」と表現しました。

さて、まだワケワカラン以下の部分をハッキリさせましょう。

instance Functor Zero where
  fmap =

圏論の知識を前提に、ネタバラシしてしまうと; 写像 $`\mrm{Zero}:{\bf Type} \to {\bf Type}`$ を関手に拡張しようということです。これは自明に出来ることですが、あえてHaskell風の「型クラスとインスタンス」の枠組みで書いてみることになります。

まずは関手に関する記法を説明しましょう。

$`F:\cat{C} \to \cat{C}`$ が関手のとき、対象パートとホムセットごとのホムパートを次のように書くことにします。

$`\quad F^\mrm{obj} : |\cat{C}| \to |\cat{C}|\\
\For a, b\in |\cat{C}|\\
\quad F^\mrm{hom}_{a, b}: \cat{C}(a, b) \to \cat{C}(F^\mrm{obj}(a), F^\mrm{obj}(b))
%`$

対象パートとすべてのホムパートが与えられて、しかるべき条件を満たすなら関手が確定します。

いま、$`f`$ を単項〈1項 | 1引数〉の型構成子だとします。これは、次のこと(すべて同値)を意味します。

  1. $`f \in {\bf TypeCons}_1`$
  2. $`f \in \mrm{Map}({\bf Type}, {\bf Type})`$
  3. $`f \in {\bf Set}({\bf Type}, {\bf Type})`$
  4. $`f \in {\bf Set}(|\cat{C}|, |\cat{C}|)`$
  5. $`f : |\cat{C}| \to |\cat{C}| \In {\bf Set}`$

したがって、単項の型構成子は $`\cat{C}`$ 上の自己関手の対象パートになり得ます。足りてないホムパートの関数達を $`g_{a, b}`$ として与えれば、全体として関手になります。与えられた $`f`$ と $`g_{a,b}`$ 達からの関手 $`F`$ の構成は次のようです。

$`\Define F^\mrm{obj} := (f : |\cat{C}| \to |\cat{C}|)\\
\For a, b\in |\cat{C}|\\
\Define F^\mrm{hom}_{a, b} := ( g_{a, b} : \cat{C}(a, b) \to \cat{C}(f(a), f(b)) )
`$

ホムパートを与える $`g`$ はいわゆる“多相関数”で、指数〈関数型 | 関数集合〉をブラケットで書いて、依存型のパイ構成 $`\prod`$ を使って書けば:

$`\quad g \in \prod_{a, b\in {\bf Type}}[f(a), f(b)]`$

依存型のシグマ構成 $`\sum`$ とセクション構成 $`\mrm{Sect}`$ を使って書けば:

$`\quad g \in \mrm{Sect}(\pi: \sum_{a, b\in {\bf Type}}[f(a), f(b)] \to {\bf Type}\times {\bf Type})\\
\quad \Where \pi \text{ は標準射影}\\
\text{i.e.}\\
\quad g:{\bf Type}\times {\bf Type} \to \sum_{a, b\in {\bf Type}}[f(a), f(b)]\\
\quad \Where \pi \circ g = \id_{{\bf Type}\times {\bf Type}}
%`$

もともとあった型構成子 $`f`$ に加えて、上記のごとき多相関数 $`g`$ があれば、それを素材に関手 $`F`$ を組み立てられるわけです*3

型クラスとそのインスタンス

前節では、関手の記述のために3つの名前 $`f, g, F`$ が出てきています。また、圏論的メカニズムは、人によっては鬱陶しくて知りたくもない事かも知れません。「名前が増えすぎる」「背後の詳細は知りたくない」という問題・要望に対して、Haskell風の型クラスが解決策を与えます。

関手の記述を想定した型クラス Functor の定義は次のようです。

class Functor f where
  fmap :: (a -> b) -> f a -> f b

次のような意図です。

  1. $`f`$ は型構成子 $`f:{\bf Type} \to {\bf Type}`$ である。
  2. $`f`$ を対象パートとする関手を、型構成子と同じ名前 $`f`$ で呼びたい。
  3. 関手のホムパートとして追加すべき多相関数は「関手 $`f`$ の $`\mrm{fmap}`$」という呼び名で参照したい。

「関手 $`f`$ の $`\mrm{fmap}`$」を仮に $`\mrm{Functor}(f).\mrm{fmap}`$ と書くとして、そのプロファイル(域・余域の仕様)をハッキリと書けば:

$`\For f\in \mrm{Map}({\bf Type}, {\bf Type})\\
\For a, b \in {\bf Type}\\
\quad \mrm{Functor}(f).\mrm{fmap}_{a, b}: \cat{C}(a, b) \to \cat{C}(f(a), f(b))\\
\text{i.e.}\\
\quad \mrm{Functor}(f).\mrm{fmap} \in \prod_{a, b\in {\bf Type}}[f(a), f(b)]
`$

$`f`$ と $`\mrm{Functor}(f).\mrm{fmap}`$ から関手 $`F`$ は次のように定義できます。

$`\Define F^\mrm{obj} := (f : {\bf Type} \to {\bf Type})\\
\For a, b\in |\cat{C}|\\
\Define F^\mrm{hom}_{a, b} := ( \mrm{Functor}(f).\mrm{fmap}_{a, b} : \cat{C}(a, b) \to \cat{C}(f(a), f(b)) )
`$

この関手 $`F`$ も同じ名前 $`f`$ で呼ぶことにします。$`f \longleftrightarrow F`$ と1:1対応しているので、同一視してもさほど問題はありません。

こう書くと、$`\mrm{Functor}`$ が次のような写像だと思うかも知れません(以下のブラケット $`[\cat{C}, \cat{C}]`$ は、関手圏です)。

$`\quad \mrm{Functor}: \mrm{Map}({\bf Type}, {\bf Type}) \to |[\cat{C}, \cat{C}]|`$

そうではありません。任意の型構成子に、自己関手を対応付けるような写像をいつでも定義できるとは限らないので、$`\mrm{Functor}`$ は時間と共にポツリポツリと定義される部分写像だと考えます。($`\supseteq\!\to`$ は部分写像を表す矢印。)

$`\quad \mrm{Functor}: \mrm{Map}({\bf Type}, {\bf Type}) \supseteq\!\to |[\cat{C}, \cat{C}]|`$

「ポツリポツリと定義」とは、特定の型構成子に対して関手のホムパート(である多相関数)を追加する作業のことです。$`\mrm{Funtor}`$ の「ポツリポツリと定義」にはインスタンス定義構文が使われます。例えば以下は、Maybeモナドの台関手を、もとになる型構成子から定義したものです*4

data MyMaybe a = MyJust a | MyNothing

instance Functor MyMaybe where
  fmap f (MyJust x) = MyJust (f x)
  fmap f MyNothing  = MyNothing

$`\mrm{Functor}(\mrm{MyMaybe}).\mrm{fmap}`$ は次のように定義されています。以下に出現する変数 $`f`$ は型構成子ではなくて関数を表しています(そう書いてあるけど念の為)。関数の本体はパターンマッチング・ケース文で、$`=^\sim`$ はパターンマッチングをする記号です。変数 $`x`$ はパターンマッチング成功時に型 $`a`$ の値に束縛されます。

$`\For a, b \in {\bf Typ} = |\cat{C}|\\
\For f \in \cat{C}(a, b) \text{ i.e. } f:a \to b \In \cat{C}\\
\Define \mrm{Functor}(\mrm{MyMaybe}).\mrm{fmap}_{a,b}(f) := \\
\quad \lambda\, y\in \mrm{MyMaybe}(a).(\\
\qquad \text{if }(\, y =^\sim (\mrm{MyJust}\, x) \,)\text{ then } \mrm{MyJust}\, f(x)\\
\qquad \text{if }(\, y =^\sim \mrm{MyNothing} \,)\text{ then } \mrm{MyNothing}\\
\quad )
%`$

これで定義される関手も $`\mrm{MyMaybe}`$ と呼ぶので、次が成立します。

$`\quad \mrm{MyMaybe}^\mrm{obj} = \mrm{MyMaybe}\\
\quad \mrm{MyMaybe}^\mrm{hom}_{a, b} = \mrm{Functor}(\mrm{MyMaybe}).\mrm{fmap}_{a,b}
%`$

空集合からの関数

Haskell風型クラスとインスタンスにより、関手の記述が出来る事はわかりました。そうならば、

instance Functor Zero where
  fmap =

これは型構成子 $`\mrm{Zero}`$ を関手に拡張していることになります。拡張した関手も同じ名前 $`\mrm{Zero}`$ と呼ぶことにします。関手 $`\mrm{Zero}`$ のホムパートは次のようになります。(上付きの $`^\mrm{hom}`$ は省略します。)

$`\For a, b \in {\bf Type} = |\cat{C}|\\
\For f \in \cat{C}(a, b) \text{ i.e. } f:a \to b \In \cat{C}\\
\quad \mrm{Zero}_{a, b}(f) : \cat{C}(a, b) \to \cat{C}(\mrm{Zero}(a), \mrm{Zero}(b))
%`$

$`\mrm{Zero}(a) = \mrm{Zero}(b) = \emptyset`$ なので、次のように書き換えられます。

$`\quad \mrm{Functor}(\mrm{Zero}).\mrm{fmap}_{a, b}(f) = \mrm{Zero}_{a, b}(f) : \cat{C}(a, b) \to \cat{C}(\emptyset, \emptyset)`$

$`\cat{C}(\emptyset, \emptyset)`$ は空集合〈never型〉のあいだの関数の集合です。この“関数の集合”は単元集合です。つまり、

$`\quad \cat{C}(\emptyset, \emptyset) = \{\id_\emptyset\} \cong {\bf 1}`$

空集合を $`{\bf 0}`$ と書くと:

$`\quad [{\bf 0}, {\bf 0}] = {\bf 0}^{\bf 0}\cong {\bf 1}`$

$`\cat{C}(\emptyset, \emptyset)`$ の唯一の要素を $`\bot := \id_\emptyset`$ と書けば:

$`\For a, b \in {\bf Type} = |\cat{C}|\\
\Define \mrm{Functor}(\mrm{Zero}).\mrm{fmap}_{a, b} = \mrm{Zero}_{a, b} :=\\
\quad \lambda\, f\in \cat{C}(a, b).(\, \bot \;\in \cat{C}(\emptyset, \emptyset)\,)
%`$

以上で、初見でほぼワケワカランだった以下の疑似コードの意図を読み取ることができました。

data 0 a

instance Functor 0 where
  fmap =

*1:$`\emptyset \in |\cat{C}|`$ は今回の話の流れで必要なだけであって、必要ないときも多いです。

*2:「型とはなんぞや?」のような大上段に構えた疑問の提示は無意味で不毛で失礼なのでやめましょうね。絶対的な定義があるわけではなくて、あくまで立場に相対的に色々な定義があるのです。

*3:組み立てた後で、関手性の確認が必要です。

*4:モナドの場合は、モナド、その台関手、台関手の対象パートである型構成子をすべて同じ名前で呼びます。