Type: Type can lead to Russell's paradox

[ksqsf]

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.

[AliasQli]

I fixed the code and this should do:

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)
}

function equal_swap
  ( implicit A: Type
  , implicit x: A
  , implicit y: A
  , xy_equal: Equal(A, x, y)
  ):Equal(A, y, x) {
  return replace
    ( xy_equal
    , (w) => Equal(A, w, x)
    , refl
    )
}

// For every x ∈ Δ, x ∉ x. (By definition of Δ.)
function xInΔ_xNotInx(x: Set, xInΔ: In(x, Δ)): NotIn(x,x) {
  return replace
    ( equal_swap(cdr(xInΔ))
    , (s) => NotIn(s,s)
    , cdr(car(xInΔ))
    )
}

// Hence, Δ ∉ Δ.
let ΔNotInΔ: NotIn(Δ, Δ) = (ΔInΔ) => { return xInΔ_xNotInx(Δ, ΔInΔ)(ΔInΔ) }

// However, that means Δ ∈ Δ, which is absurd.
let falso: Absurd = ΔNotInΔ(xNotInx_xInΔ(Δ, ΔNotInΔ))

However, when I finally got falso, cic ran into an error:

RangeError: Maximum call stack size exceeded
    at ImplicitApCore.evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/exps/implicit-pi/implicit-ap-core.js:37:13)
    at evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/core/evaluate.js:7:16)
    at ImplicitApCore.evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/exps/implicit-pi/implicit-ap-core.js:38:57)
    at evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/core/evaluate.js:7:16)
    at ImplicitApCore.evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/exps/implicit-pi/implicit-ap-core.js:38:57)
    at evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/core/evaluate.js:7:16)
    at ApCore.evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/exps/pi/ap-core.js:36:49)
    at evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/core/evaluate.js:7:16)
    at ApCore.evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/exps/pi/ap-core.js:36:49)
    at evaluate (/home/user/.local/lib/node_modules/@cicada-lang/cicada/lib/lang/core/evaluate.js:7:16)

Which I think is because cic can't handle a value with type Absurd.

[ksqsf]

Actually, Cicada can have Absurd-typed terms. Just abuse the bug in #11 :

datatype WTF {
  wtf: Absurd
}
check! WTF.wtf: Absurd

[xieyuheng]

@ksqsf @AliasQli Thanks guys!

Great works.

I will learn about this example, and add it to The Manual.