データ型と型シノニム

HaskellやMLで、データ型と型シノニムの違いがある。この違いは、関数定義において、“再帰スキーマやイプシロン式で定義する”のと、“通常の関数定義する”のとの違いと類似だろう。スキーマとは、「これこれの性質を持つモノ」という性質記述をすると、その存在物を取り出す手順のこと。背後にはなんらかの一意存在定理がある。一意存在定理がないと、性質記述からモノを取り出せない。

スキーマを使う定義は、コンプリヘンションによる定義と言ってもいい。それに対して、通常の定義は組み合わせ（コンビネーション）方式と言える。

• コンプリヘンション：素材はない。なにもないところからモノを出現させる。
• コンビネーション：素材がある。それらの素材を組み合わせて作る。

再帰が不動点だからか、再帰関係は不動点の一意存在定理に頼る気がする。

イプシロンスキーマは不動点と違うが、イプシロンなしでは関数の最初の定義ができない。関数のイプシロンによる定義は、引き算の定義、割り算の定義、平方根の定義などで使われる。モノイドの単位元に名前を付けられる、群の逆元を関数と思える、などもイプシロンがあるからこそ出来ることだ。

関数定義も、スキーマによって無から引っ張り出すのと、既存の材料の組み合わせは区別すべきかもしれない。CoqのDefinitionとFixpointはそういう差か。