sign/proc定式化

ゴチャゴチャとメモ。

指標の同義語類義語

1. シグネチャ＠ML
2. インターフェイス＠オブジェクト指向言語
3. コンセプト＠C++
4. 型クラス＠Haskell
5. 型クラス＠Coq
6. モジュール＠Objファミリー

手続きの同義語類義語

1. ファンクタ＠ML
2. アダプター＠デザインパターン
3. 型パラメータ付きクラス＠オブジェクト指向言語

リテラル手続きの同義語類義語

1. ストラクチャ＠ML
2. 構造体＠C系言語
3. オブジェクト＠JSON
4. クラス＠オブジェクト指向言語
5. ライブラリモジュール＠多くのプログラミング言語

部分手続きの同義語類義語

1. 抽象クラス＠オブジェクト指向言語
2. 延期クラス＠Eiffel

部分手続きは、挿入〈insertion〉を左脚とするクライスリ圏のスパンなので、ナローイングを左余脚とする手続きの圏のコスパン。スパンの拡張＝コスパンの余拡張〈持ち上げ〉を、どちらも拡張を呼ぶ。

手続きをソフト実装、モデルをハード実装とも呼ぶ。単に実装といった場合はソフト実装。

• モデル＝ハード実装
• 手続きを＝ソフト実装＝実装

指標の構文

伝統的	圏論的
sort	0-mor
operation	1-mor
equation	2-mor
value	1-mor
predicate	1-mor

signature OrderedMonoid {
  sort U
  operation m:(U, U) → U
  value e: U
  predicate (≦):(U, U)
  // ...
}

signature OrderedMonoid {
  0-mor U
  1-mor m:U×U → U
  1-mor e:Unit → U
  1-mor (≦):U×U → Bool
  // ...
}

基本データ型は、MLのデータ型を先頭大文字：

1. Int
2. Char
3. Real
4. String
5. Bool = {True, False}

他に、

1. Unit = Void
2. Nat
3. Never

手続きの構文

procedure 名前 produces 余域指標 from 域指標 {本体}
procedure 名前 implements 余域指標 from 域指標 {本体}

略記規則

1. 無名指標では名前を省略可能。signature {...}
2. 指標が入る文脈では signature を省略可能。{...}
3. 1-宣言文（コロン1個）先頭の value を省略可能 {x:X, y:Y }
4. 基本型の {_:T} は裸の名前 T でよい。
5. 基本型 S, T の {_1:S, _2:T} は (S, T) でよい。

procedure norm produces Real from (Real, Real) {
  _ := sqrt(_1^2 + _2^2)
}

signature XY {
  value x:Real
  value y:Real
}
sinature Z {
  value z:Real
}

procedure norm produces Z from XY {
  z := sqrt(x^2 + y^2)
}

さらなる省略規則

1. from と produces の順序はどうでもよい。
2. produces は -> で置き換え可能。
3. from は省略可能。
4. _ := は省略可能。

procedure norm from (Real, Real) -> Real {
  sqrt(_1^2 + _2^2)
}

procedure norm (Real, Real) -> Real {
  sqrt(_1^2 + _2^2)
}

procedure norm -> Real (Real, Real) {
  sqrt(_1^2 + _2^2)
}