Type: Type can lead to Russell's paradox #12
Description
The following piece of code is a direct replay of The Trouble of Typing Type as Type in Cicada.
datatype Set {
set(X: Type, y: (X) -> Set): Set
}
function carrier(s: Set): Type {
return induction(s) {
(_) => Type
case set(x, _) => x
}
}
function index(s: Set): (carrier(s)) -> Set {
return induction(s) {
(s) => (carrier(s)) -> Set
case set(_, y) => y
}
}
function In(a: Set, b: Set): Type {
return [ x : carrier(b) | Equal(Set,a,index(b)(x)) ]
}
function NotIn(a: Set, b: Set): Type {
return (In(a, b)) -> Absurd
}
let Δ = Set.set([s: Set| NotIn(s,s)], (pair) => car(pair))
check! Δ: Set
// For every x ∉ x, x ∈ Δ. (By definition of Δ.)
function xNotInx_xInΔ(x: Set, xNotInx: NotIn(x, x)): In(x, Δ) {
return cons(cons(x, xNotInx), refl)
}
// For every x ∈ Δ, x ∉ x. (By definition of Δ.)
function xInΔ_xNotInx(x: Set, xInΔ: In(x, Δ)): NotIn(x,x) {
return cdr(car(xInΔ))
}
// Hence, Δ ∉ Δ.
let ΔNotInΔ: NotIn(Δ, Δ) = (ΔInΔ) => { return xInΔ_xNotInx(Δ, ΔInΔ) }
// However, that means Δ ∈ Δ, which is absurd.
let falso: Absurd = ΔNotInΔ(xNotInx_xInΔ(Δ, ΔNotInΔ))
However, the type checker rejects the code above for dubious reasons:
I infer the type to be:
(_: [x1: induction (car(car(xInΔ))) { (_) => Type case set(x1, _) => x1 } | Equal(Set, car(car(xInΔ)), induction (car(car(xInΔ))) { (s1) => (_: induction (s1) { (_) => Type case set(x2, _) => x2 }) -> Set case set(_, y, _1) => y(_1) }(x1))]) -> Absurd
But the expected type is:
(_: [x1: induction (x) { (_) => Type case set(x1, _) => x1 } | Equal(Set, x, induction (x) { (s1) => (_: induction (s1) { (_) => Type case set(x2, _) => x2 }) -> Set case set(_, y, _1) => y(_1) }(x1))]) -> Absurd
Paradox.cic:
39 |
40 |// For every x ∈ Δ, x ∉ x. (By definition of Δ.)
41 |function xInΔ_xNotInx(x: Set, xInΔ: In(x, Δ)): NotIn(x,x) {
42 | return cdr(car(xInΔ))
43 |}
44 |
I'm not sure how to show car(car(xInΔ))) is definitionally equivalent to x in this context, but I think it is perfectly valid to say car(car(xInΔ))) == x. And the root cause of inconsistency (if ever proved) here is Type : Type, which is accepted by the type checker.