導入と除去の規則

型の導入規則とは、型の生成規則で、型だけではなくて要素の構成規則も含む。

  • 型を型構成子で生成する。
  • 要素を要素〈値〉構成子で生成する。要素生成子は関数である。

型の除去規則とは、型の消費規則で、関数による要素の構成規則(「構成」で間違ってない)も含む。

  • 既に型構成子で生成した型と要素がある。
  • その型の要素に関数を後結合子て消費すると、中間の型を除去した(カットした)要素が得られる。

次のようにも言える。

  • 導入規則は、複合型を域とする関数の構成法を与える。当該複合型の新しい証拠を生成する。
  • 除去規則は、複合型を余域とする関数の構成法を与える。当該複合型の既存証拠を消費して、新しい証拠を作る。
  • 複合型には、アロー型、依存アロー型、直積型〈タプル型〉、直和型〈タグ付きユニオン型〉、一般的帰納的型がある。
  • 一般的帰納的型の導入規則と除去規則は難しくなる。簡単な例はタグ付きユニオン型の、値コンストラクタとパターンマッチ分岐処理。

規則はコンビネータであり、そのコンビネータを使うコマンドでもある。また、関数は後結合/前結合でコンビネータとみなすことができる。And.intro は関数だが、And.introを後結合するコンビネータ doPostComp And.intro でもあり、コンビネータを入力シーケントに適用するコマンドでもある。