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)
}