なんというバカバカしさ、なんという無駄、なんという浪費!
ラムダ計算 | インスティチューション | 型理論 |
---|---|---|
型コンテキスト | 指標 | 型前提(域側) |
大きなラムダ式 | クライスリ指標射 | 型判断(シーケント) |
大きなラムダ計算 | 指標圏の計算 | 型証明計算 |
レコード(値環境) | 点指標射(指標圏の点射) | 型証拠(ハビテーション) |
レコードの圏 | ソフトモデル圏(指標コスライス) | - |
プログラミング:
インスティチューション | 関数型 | オブジェクト指向 | データベース |
---|---|---|---|
指標 | 型クラス, 指標 | インターフェイス | テーブルスキーマ |
クライスリ指標射 | ファンクタ | アダプターパターン | データマイグレーション |
指標圏の計算 | - | - | - |
点指標射(指標圏の点射) | ストラクチャ, レコード | クラスインスタンス | テーブル行 |
ソフトモデル圏 | ストラクチャとファンクタ | アダプタープログラミング | - |
集約・統合・圧縮のとき、けっこう邪魔になるのが、要素と点の違い。
- 要素: 集合論的な実体(モノ)
- 点 = 点射 : 終対象または単位対象からの射
それと、指数型の対象とホムセットの混同、つまり、指数対象への点射と、反カリー化した射の区別が出来ない。