トップ «前の日記(2006-11-13) 最新 次の日記(2006-11-15)» 月表示 編集

日々の流転


2006-11-14 [長年日記]

λ. Haskell Bowling by Ron Jeffries

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

Tags: haskell

λ. 強い直和?

強い直和(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 でも同じ間違いをしていた。

関連

Tags: 型理論
本日のツッコミ(全2件) [ツッコミを入れる]
ψ sumii (2006-11-26 14:00)

全然門外漢なので外しているかもしれませんが、最後の(λa:A. λb:B. b)はどう型付けできるのでしょうか?

ψ さかい (2006-11-26 15:51)

ありがとうございます。お陰で解決しました。<br>ここでは (λa:A. λb:B. b) の型が (Πa:A. B → B[a := fst t]) にならないといけないですが、これが成り立たないのですね。<br><br>> 全然門外漢なので外しているかもしれませんが<br>型理論の専門家でない私のような人から見れば、sumiiさんは全然門外漢ではないと思います。