トップ «前の日記(2011-08-07) 最新 次の日記(2011-08-26)» 月表示 編集

日々の流転


2011-08-25 [長年日記]

λ. "The Arrow Calculus" by Sam Lindley, Philip Wadler, Jeremy Yallop

を読んだ。

ArrowはこれまでHughesのオリジナルのようにポイントフリーに形式化され、Patersonのアロー記法(Arrow notation)はただのシンタックスシュガーという扱いだったが、この論文ではPatersonのアロー記法に基づいた計算体系と型システムとを作り、両者の形式化が等しいことを証明している。 二つの文脈を使って、通常の変数束縛とアローで束縛された変数を区別するのは、よくありそうだけど、よく出来てるなぁ。

また、その副産物として、オリジナルのArrowの公理が冗長だったことが分かった。 f >>> arr id = f はArrowの他の公理から導出可能だし、 first (arr (g>>>)) >>> app = second g >>> app はArrowApplyの他の公理から導出可能。 これには驚いた。