未だに、線形論理の何が凄いのかよく分からないけど、そもそも、logicsの素養がないし、sequent calculusとかキライなので、そっち方面から理解しようとするのは間違いだと気付いた。というか、昨日まで、Curry-Howard同形で、対応するラムダ計算があること…

1. 形式意味論がないのに「偽のスタート」を切っている。 2. パラダイム戦争のために言語は使われない。 3. 型推論も遅延評価も飛躍的な進歩というわけじゃない。 4. プログラマは保守的かつ貪欲で動機がない。 5. GHCは世界を救わない。 6. 関数型言語ではL…

Wadlerのノートにあった Lfix X. F X = All X. (F X -> X) -> X. Gfix X. F X = Exists X. (X -> F X) * X. という定義はどっから降ってきたのかというと、単に、こういう話のような。 以下、fをFunctor、inF::f(Fix(f))->Fix(f)として、 buildF::(forall x.…