日々の流転

λ. Haskell Bowling by Ron Jeffries

<URL:http://d.hatena.ne.jp/machi_pon/20061104> より。 実はこれまでボーリングのスコアの定義を知らなかったのだけど、こういう風に定義されているのか。

λ. 強い直和?

強い直和(strong sum)とCCに関して混乱中。

強い直和と弱い直和

以下の推論規則からなる型を「強い直和」と呼ぶ。

Γ, a : A ├ B : *
──────────
Γ ├ (Σa:A. B) : *

Γ ├ t : A   Γ ├ u : B[a := t]
─────────────────
Γ ├ (t,u) : Σa:A. B

Γ ├ t : (Σa:A. B)
───────────
Γ ├ fst t : A

Γ ├ t : (Σa:A. B)
──────────────
Γ ├ snd t : B[a := fst t]

それに対して、この推論規則の最後の二つを以下の推論規則で置き換えたものを「弱い直和」と呼ぶ。

Γ ├ t : (Σa:A. B)  Γ ├ C : *  Γ ├ e : (Πa:A. B→C)
─────────────────────────────
Γ ├ elimSum t e : C

CCと強い直和

CCには強い直和は含まれないが、弱い直和は以下のようにCC内で定義できる。

Σa:A. B = ΠX:*. (Πa:A. B → X) → X
(t,u) = λX:*. λe:(Πa:A. B → X). e t u
elimSum t e = t C e

そして、CCに強い直和を追加するとGiraldの逆説が成り立つことになっている。

が

しかし、強い直和も以下のようにCC内で定義できる気が……間違っているのはどこだ?

fst t = t A (λa:A. λb:B. a)
snd t = t ((λa:A. B) (fst t)) (λa:A. λb:B. b)

まとめ

sumiiさんの指摘でようやく理解できたが、(λa:A. λb:B. b) の型付けに問題があるのが原因だった。実際、Agdaで以下のように書いてみても、最後のゴールがrefine出来ない。AgdaはCCのようなimpredicativeな言語ではないけど、この例が型付けできないことを示すには十分だろう。

Sum :: (A::Set) -> (A->Set) -> Type
Sum A B = (X::Set) -> ((a::A) -> B a -> X) -> X

pair (|A::Set) (|B::A->Set) :: (a::A) -> B a -> Sum A B
pair a b = \(X::Set) -> \(f::(a'::A) -> B a' -> X) -> f a b

elimSum (|A::Set) (|B::A->Set) (|X::Set)
    :: Sum A B -> ((a::A) -> B a -> X) -> X
elimSum t f = t X f

fst (|A::Set) (|B::A->Set) :: Sum A B -> A
fst t = t A (\(a::A) -> \(b::B a) -> a)

snd (|A::Set) (|B::A->Set) :: (t::Sum A B) -> B (fst t)
snd t = t (B (fst t)) (\(a::A) -> \(b::B a) -> {! b !})

ちなみに、The Theory of Parametricity in Lambda Cube でも同じ間違いをしていた。

関連

• ECC, an Extended Calculus of Constructions - ECCはCCを拡張して強い直和を導入した型理論