昨日の記事「記号のグリフと使用場面・使用意図： 型理論、圏論、集合論、論理など」より：
なんでそこまでコロンとターンスタイルにこだわるのか？ 僕にはちょっと意味不明です。
...[snip]...
僕の個人的感想としては、型理論独自の記法をやめて、圏論と集合論の記法で書き換えてしまえばスッキリすると思うのですが ‥‥
コロンとターンスタイル、それとカンマを激しくオーバーロードして、いったい誰が得するのかな？ 書く側が楽ちんというメリットは確かにありますが、読む側の負担を考えると、ほんとやめたほうがいいと思う。$`
%\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\In}{\text{ in }}
\newcommand{\dto}{\mathrel{!\!{\to}} }
\newcommand{\dtimes}{\mathrel{!\!{\times}} }
%\newcommand{\Imp}{\Rightarrow }
%\newcommand{\Iff}{\Leftrightarrow }
%\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\hyp}{\text{－} }
%\newcommand{\twoto}{\Rightarrow }
%\newcommand{\id}{\mathrm{id} }
%\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\cons}{\mathop{\blacktriangleright} }
\newcommand{\snoc}{\mathop{\blacktriangleleft} }
%\require{enclose}
`$
内容：
はじめに
例えば、二項演算を含む指標のオペレーション宣言を型理論の判断形式〈judgement form〉で書くと次のようになります。
$`\quad (x: \msf{U}, y: \msf{U}) \vdash \msf{m}(x, y) : \msf{U}`$
使われている記号は、コロン（'$`:`$'）とターンスタイル（'$`\vdash`$'）です。これを次の形式に書いたら何か悪いことが起きるのでしょうか？
$`\quad (x\in \msf{U}, y\in \msf{U}) \mapsto \msf{m}(x, y) \in \msf{U}`$
あるいは、より圏論風にして次の形式だとなにがダメなんでしょう？
$`\quad \msf{m} : (x\in \msf{U}, y\in \msf{U}) \to \msf{U}`$
コロンとターンスタイルに慣れている人には、$`\in, \mapsto, \to`$ が気持ち悪いってのは確かにあるでしょう。ですが、'$`\in`$' をコロンに、'$`\mapsto`$' や '$`\to`$' をターンスタイルに置き換えるのは容易です。
'$`\in`$' や '$`\to`$' を使うとセマンティクスが変わってしまう、あるいはセマンティクスが正しく伝わらない、ということは確かにあります。そのときは、'$`\in`$' や '$`\to`$' が不適切なわけですから、別な記号を使えばいいだけです。
コロンのオーバーロード回避の案
- 集合論の所属関係とみなせる場合は、コロンの代わりに '$`\in`$' を使う。
- 所属に近いが、「外延性が成立しない」など所属とはみなせない場合は '$`\in:`$' を使う。
- コロン1個、またはコロンを何個か並べた記号は、圏論のプロファイルコロン（「記号のグリフと使用場面・使用意図： 型理論、圏論、集合論、論理など」参照）の意味で使う。
- 型が型宇宙に居住することを示すには、コロンの代わりに '$`\text{in}`$' を使う。
- 等式 $`M = N`$ が型 $`A`$ 上で成立していることを表すには、コロンの代わりに $`\text{holds }M = N \text{ on }A`$ （コロンの位置に $`\text{on}`$）を使う。
型コンテキストのなかの型宣言において、 $`x: X`$ を $`x\in X`$ と書きたくない理由として、「$`x\in X`$ は集合論の命題だが、宣言は命題ではない」ということはあるでしょう。確かにそうなんですが、型コンテキストは宣言の集まりだと規定されているのだから、気にするほどの問題じゃないと思います。
「宣言と命題は違うんだ」という話は至るところで出てくるので、コロンを使って識別する方法だけではどうせ解決できないし。
ターンスタイルのオーバーロード回避の案
ターンスタイル '$`\vdash`$' を '$`\to`$' に変えてしまうとセマンティクスが変わってしまうケースとして、ターンスタイルで依存性を表現していることがあります。パイ型、つまり依存関数達の集合を構成する演算として $`[\hyp\dto\hyp]`$ も使うことにします。
$`\quad [(x\in X) \dto F(x)] := \prod_{x\in X}F(x)`$
また、次の書き方の約束をします。
$`\quad f : (x\in X) \dto F(x) \iff f\in [(x\in X) \dto F(x)]`$
'$`\dto`$' を使うと依存関数のプロファイル宣言が書けることになります。普通の関数は依存関数の特別なものなので、普通の関数のプロファイル宣言に '$`\dto`$' を使っても別にかまいません。
- ターンスタイルは、依存関数のプロファイル宣言に使う。つまり、'$`\vdash`$' は '$`\dto`$' と同義だとする。依存性がない関数のプロファイル宣言に使ってもよい。
- 整形式性〈well-formedness〉のような構文的な宣言には、ターンスタイルではなくて '$`\Vdash`$' を使う。例えば $`\Gamma \vdash`$ （右側に何も書かない）ではなくて $`\Vdash \Gamma`$ とか。
- 判断を文〈構文的対象〉とする演繹系（「演繹系とオペラッド」参照）に対するメタレベルの導出可能性には、ターンスタイルではなくて '$`\Vvdash`$' を使う。
- 依存関数の宣言でもなく、構文的な宣言でもなく、導出可能性でもない意味で使う場合は、なんか別な記法を使う。ターンスタイルの流用はやめる。
カンマのオーバーロード回避の案
カンマは、構文定義の際のリスト処理の演算記号として使われます。区切り記号としてのカンマと紛らわしくて僕は不快です。また、シグマ型を構成する演算記号としても使われます。
- リスト処理のコンス演算（リストの先頭に項目追加）の演算記号としては、カンマではなくて '$`\cons`$' を使う。
- リスト処理のスノック演算（リストの末尾に項目追加）の演算記号としては、カンマではなくて '$`\snoc`$' を使う。
- リスト処理の連接演算（2つのリストを繋ぐ）の演算記号としては、カンマではなくて '$`\#`$' を使う。
- シグマ型を構成する演算記号としては、カンマではなくて '$`\dtimes`$' を使う。
$`\dtimes`$ の定義は次のようです。
$`\quad (x\in X) \dtimes F(x) := \sum_{x\in X}F(x)`$
依存性がない場合は $`\hyp\times\hyp`$ と $`[\hyp\to\hyp]`$ 、依存性があるかも知れない場合は $`\hyp\dtimes\hyp`$ と $`[\hyp\dto\hyp]`$ です。
空リストは様々な場面で重要な役割りを演じますが、空リストの書き方も困ることがあるので約束をしておきます。
- 何も書かないことで空リストを表すのはやめる。
- 空リストは、$`()`$ 、$`\langle \rangle`$ などで明示的に書く。
- 空リストを、$`\cdot, *, \diamond`$ などの記号で表すときは、その旨を明示する。
よくある $`\vdash t: A`$ のような書き方は、ターンスタイルの右側に空リストがあります。空リストをちゃんと書けば：
$`\quad () \vdash t: A`$
集合論的／圏論的な記法で書けば、次のいずれかです。
$`\quad () \mapsto t \in A`$
$`\quad t: () \to A`$
空リストを '$`\diamond`$' で書くならば：
$`\quad \diamond \mapsto t \in A`$
$`\quad t: \diamond \to A`$
空リストにはややこしい面があります。
- 仮引数リストとしての空リストは、実引数データとしての空リストではない。
- 仮引数リストとしての空リストの集合論的意味は、なんらかの単元集合である。
- 単元集合の唯一の要素が空リストだと約束する場合がある。
- 空リストと、空リストだけからなる単元集合が同一視されることがある。
空リスト、空集合、単元集合などはシッカリ区別しましょう。区別したうえでの適宜同一視はかまいません。
おわりに
色々な記号を使い分けたり、囲み括弧を律儀に付けたりすると、書くのが面倒くさいだけでなく、出来上がりの見た目が鬱陶しくて汚いものになります。面倒くさくて汚いということが、人をオーバーロードと省略に向かわせる大きな要因かも知れません。
ただ、最初から審美的要求を優先させるのはいかがなものでしょう。最初は、面倒くさくて汚いところから始めて、十分に慣れた後で、簡潔さや美しさを追求すればいいんじゃないの。
