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.
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.