今風の型理論入門（本編） - 檜山正幸のキマイラ飼育記 (はてなBlog)前ふりは「型→代数→…それから：型理論入門（の前半）」にあります。これは本編（後半）。1回読み切り（長いけど）で、比較的新しい*1型理論を紹介します。「入門（門に入る）」というよりは門の外から中を覗いてみる程度。 説明用コードはJavaの構文を使います。ただし、パッケージ宣言は書かないし、publicはなるべく省略。 内容： インターフェースなんて、所詮こんなもの 心理的効果とか、人間-人間コミュニケーションとかは、別問題 わけわからんインターフェースに制約を付加する もっと制約を足してみる 謎のインターフェースに意図されたもの で、それが型理論にどうつながるの？ インターフェースなんて、所詮こんなもの まず、次のインターフェースを見てください。 interface AB { int a(); void b(); } これスゴイでしょ。何がスゴイって、これを見てもなんのことやらサッパリわか
