日々の流転

λ. "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の他の公理から導出可能。 これには驚いた。