4 ms·
I recognise it as the type of continuation returning something of type a. Also, if you instantiate r to Void then ((a -> Void) -> Void) <-> a is just double n
by Chattered 12y ago
I recognise it as the type of continuation returning something of type a. Also, if you instantiate r to Void then
((a -> Void) -> Void) <-> a
is just double negation elimination.
Am I getting sidetracked or does this line go somewhere, tel?
- tel 12y agoYou're totally correct that double-negation elimination is a specialization of the CPS transform which is a specialized form of Yoneda. Yoneda is more general and exists more often than CPS transforms do, though. cps : a -> (forall r . (a -> r) -> r) cps a = \f -> a f cps' : (forall r . (a -> r) -> r) -> a cps' f = f id It's interesting to examine double negation elimination in constructivist logic since it doesn't hold there. In particular, we can easily write the backward direction bck : a -> ((a -> Void) -> Void) bck = cps a but since we've now specialized `forall r` to `Void` we can no longer come back. This demonstrates (1) that the pure CPS'd version is more general than DNE and (2) proof by contradiction is non-constructive.
- tel 12y agoTypo: `bck` should obviously be bck = cps