Why is this computable?

Stream: general

[Kenny Lau]

why on earth is this computable?

def prod' : Type → Type → Type :=
λ α β, classical.choice ⟨α × β⟩

[Kenny Lau]

and why on earth is this noncomputable?

noncomputable def prod' : Type → Type → ℕ :=
λ α β, classical.choice ⟨0⟩

[Mario Carneiro]

types are erased

[Kenny Lau]

types are what?

[Mario Carneiro]

they are not data

[Kenny Lau]

:o

[Mario Carneiro]

you can't compute with them

[Kenny Lau]

what is data?

[Kenny Lau]

this is new

[Mario Carneiro]

in the VM they are unit

[Kenny Lau]

I always thought that only Prop is not data

[Mario Carneiro]

proofs and types are not data

[Mario Carneiro]

everything else is

[Mario Carneiro]

as a result, proofs and types are always vacuously computable

[Kenny Lau]

why is Type not data?

[Mario Carneiro]

because types are not observable in the lambda calculus

[Mario Carneiro]

you can delete all the types and all the lambdas make sense

[Gabriel Ebner]

Another good reason is that there is no sensible return value for the noncomputable version, after all, all existence proofs here are definitionally equal:

example : classical.choice ⟨0⟩ = classical.choice ⟨1⟩ :=
rfl

[Kenny Lau]

and what's a sensible return value for the computable version?

[Mario Carneiro]

empty?

[Mario Carneiro]

or anything

[Mario Carneiro]

Here's an amusing example:

import tactic.interactive

def T : Type := if classical.choice ⟨0⟩ = 0 then ℕ else ℕ

def three : T := cast (by unfold T; split_ifs; refl) 3

#eval three -- #3

it uses a noncomputable type, and a noncomputable proof, and gets something computable and can actually be #eval'd

[Mario Carneiro]

and what's a sensible return value for the computable version?

Actually a better answer is "unit star" because in the VM Type = unit

[Kenny Lau]

oh hell