If you write me a function of type (a→⊥)→⊥, I can point out the place in its source code where you included a value of type a, but I can’t write a function of type ((a→⊥)→⊥)→a.
I think I must’ve not paid enough attention in type theory class to get this? Is this an excluded middle thing? (if it’s a joke that I’m ruining by asking this feel free to let me know)
Look, there’s an integer! It’s right there, “4”. Apparently Int is inhabited.
bar :: ((a→⊥)→⊥)→a bar fo = ???
There’s nothing in particular to be done with fo… if we had something of type a→⊥ to give fo, we would be open for business, but we don’t know enough about a to make this any easier than coming up with a value of type ⊥, which is a non-starter.
I am giving an example of something I can do “for any x” but not “for all x”. In the first case, the x is given in a fully constructed, reified form, and I can look at its internals to build a bespoke response. In the second case, I would have to give a general procedure that can work with all x while interacting with the x only by means of its external interface.
Ah okay, I think I understand, if I’m remembering my type theory correctly. I think this is downstream of “standard type theory” i.e. type theory created by Löf not accepting the excluded middle? Which does also mean rejecting choice, for sure.
EDIT: But fwiw, I think the excluded middle is much less controversial than Choice (it should technically be strictly less controversial). I think that may be a less interesting post, but I’m sure philosophers have already written that. Though I think a post defending rejecting the excluded middle from a type theory perspective actually could be quite good, because lots of people don’t seem to understand the arguments from the other side here, and think they’re just being ridiculous.
If you write me a function of type (a→⊥)→⊥, I can point out the place in its source code where you included a value of type a, but I can’t write a function of type ((a→⊥)→⊥)→a.
I think I must’ve not paid enough attention in type theory class to get this? Is this an excluded middle thing? (if it’s a joke that I’m ruining by asking this feel free to let me know)
foo :: (Int→⊥)→⊥
foo f = f 4
Look, there’s an integer! It’s right there, “4”. Apparently Int is inhabited.
bar :: ((a→⊥)→⊥)→a
bar fo = ???
There’s nothing in particular to be done with fo… if we had something of type a→⊥ to give fo, we would be open for business, but we don’t know enough about a to make this any easier than coming up with a value of type ⊥, which is a non-starter.
Sorry, I think explaining without using type theory what you are trying to say may help me understand better?
EDIT: like, in particular, insofar as its relevant to the axiom of choice.
I am giving an example of something I can do “for any x” but not “for all x”. In the first case, the x is given in a fully constructed, reified form, and I can look at its internals to build a bespoke response. In the second case, I would have to give a general procedure that can work with all x while interacting with the x only by means of its external interface.
Ah okay, I think I understand, if I’m remembering my type theory correctly. I think this is downstream of “standard type theory” i.e. type theory created by Löf not accepting the excluded middle? Which does also mean rejecting choice, for sure.
EDIT: But fwiw, I think the excluded middle is much less controversial than Choice (it should technically be strictly less controversial). I think that may be a less interesting post, but I’m sure philosophers have already written that. Though I think a post defending rejecting the excluded middle from a type theory perspective actually could be quite good, because lots of people don’t seem to understand the arguments from the other side here, and think they’re just being ridiculous.