Zulip Chat Archive

Stream: general

Topic: Why is this computable?


view this post on Zulip Kenny Lau (Feb 19 2019 at 08:25):

why on earth is this computable?

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

view this post on Zulip Kenny Lau (Feb 19 2019 at 08:26):

and why on earth is this noncomputable?

noncomputable def prod' : Type  Type   :=
λ α β, classical.choice 0

view this post on Zulip Mario Carneiro (Feb 19 2019 at 08:26):

types are erased

view this post on Zulip Kenny Lau (Feb 19 2019 at 08:27):

types are what?

view this post on Zulip Mario Carneiro (Feb 19 2019 at 08:27):

they are not data

view this post on Zulip Kenny Lau (Feb 19 2019 at 08:27):

:o

view this post on Zulip Mario Carneiro (Feb 19 2019 at 08:27):

you can't compute with them

view this post on Zulip Kenny Lau (Feb 19 2019 at 08:27):

what is data?

view this post on Zulip Kenny Lau (Feb 19 2019 at 08:27):

this is new

view this post on Zulip Mario Carneiro (Feb 19 2019 at 08:27):

in the VM they are unit

view this post on Zulip Kenny Lau (Feb 19 2019 at 08:27):

I always thought that only Prop is not data

view this post on Zulip Mario Carneiro (Feb 19 2019 at 08:27):

proofs and types are not data

view this post on Zulip Mario Carneiro (Feb 19 2019 at 08:27):

everything else is

view this post on Zulip Mario Carneiro (Feb 19 2019 at 08:28):

as a result, proofs and types are always vacuously computable

view this post on Zulip Kenny Lau (Feb 19 2019 at 08:29):

why is Type not data?

view this post on Zulip Mario Carneiro (Feb 19 2019 at 08:30):

because types are not observable in the lambda calculus

view this post on Zulip Mario Carneiro (Feb 19 2019 at 08:30):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 19 2019 at 08:32):

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

view this post on Zulip Mario Carneiro (Feb 19 2019 at 08:32):

empty?

view this post on Zulip Mario Carneiro (Feb 19 2019 at 08:32):

or anything

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 19 2019 at 08:40):

oh hell


Last updated: May 10 2021 at 00:31 UTC