## Stream: general

### Topic: Why is this computable?

#### Kenny Lau (Feb 19 2019 at 08:25):

why on earth is this computable?

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


#### Kenny Lau (Feb 19 2019 at 08:26):

and why on earth is this noncomputable?

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


types are erased

types are what?

#### Mario Carneiro (Feb 19 2019 at 08:27):

they are not data

:o

#### Mario Carneiro (Feb 19 2019 at 08:27):

you can't compute with them

what is data?

this is new

#### Mario Carneiro (Feb 19 2019 at 08:27):

in the VM they are unit

#### Kenny Lau (Feb 19 2019 at 08:27):

I always thought that only Prop is not data

#### Mario Carneiro (Feb 19 2019 at 08:27):

proofs and types are not data

#### Mario Carneiro (Feb 19 2019 at 08:27):

everything else is

#### Mario Carneiro (Feb 19 2019 at 08:28):

as a result, proofs and types are always vacuously computable

#### Kenny Lau (Feb 19 2019 at 08:29):

why is Type not data?

#### Mario Carneiro (Feb 19 2019 at 08:30):

because types are not observable in the lambda calculus

#### Mario Carneiro (Feb 19 2019 at 08:30):

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

#### Gabriel Ebner (Feb 19 2019 at 08:30):

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 (Feb 19 2019 at 08:32):

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

#### Mario Carneiro (Feb 19 2019 at 08:32):

empty?

or anything

#### Mario Carneiro (Feb 19 2019 at 08:35):

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 (Feb 19 2019 at 08:37):

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 (Feb 19 2019 at 08:40):

oh hell

Last updated: May 10 2021 at 00:31 UTC