[Haskell-cafe] Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)
Ruben Astudillo
ruben.astud at gmail.com
Fri May 15 09:19:01 UTC 2020
On 13-05-20 09:15, Olaf Klinke wrote:
> Excersise: Prove that intuitionistically, it is absurd to deny the law
> of excluded middle:
>
> Not (Not (Either a (Not a)))
It took me a while but it was good effort. I will try to explain how I
derived it. We need a term for
proof :: Not (Not (Either a (Not a)))
proof :: (Either a (Not a) -> Void) -> Void
A first approximation is
-- Use the (cont :: Either a (Not a) -> Void) to construct the Void
-- We need to pass it an Either a (Not a)
proof :: (Either a (Not a) -> Void) -> Void
proof cont = cont $ Left <no a to fill in>
Damn, we can't use the `Left` constructor as we are missing an `a` value
to fill with. Let's try with `Right`
proof :: (Either a (Not a) -> Void) -> Void
proof cont = cont $ Right (\a -> cont (Left a))
Mind bending. But it does make sense, on the `Right` constructor we
assume we are have an `a` but we have to return a `Void`. Luckily we can
construct a `Void` retaking the path we were gonna follow before filling
with a `Left a`.
Along the way I had other questions related to the original mail and
given you seem knowledgeable I want to corroborate with you. I've seen
claimed on the web that the CPS transform *is* the double negation [1]
[2]. I don't think that true, it is almost true in my view. I'll
explain, these are the types at hand:
type DoubleNeg a = (a -> Void) -> Void
type CPS a = forall r. (a -> r) -> r
We want to see there is an equivalence/isomorphism between the two
types. One implication is trivial
proof_CPS_DoubleNeg :: forall a. CPS a -> DoubleNeg a
proof_CPS_DoubleNeg cont = cont
We only specialized `r ~ Void`, which mean we can transform a `CPS a`
into a `DoubleNeg a`. So far so good, we are missing the other
implication
-- bind type variables: a, r
-- cont :: (a -> Void) -> Void
-- absurd :: forall b. Void -> b
-- cc :: a -> r
proof_DoubleNeg_CPS :: forall a. DoubleNeg a -> CPS a
proof_DoubleNeg_CPS cont = \cc -> absurd $ cont (_missing . cc)
Trouble, we can't fill `_missing :: r -> Void` as such function only
exists when `r ~ Void` as it must be the empty function. This is why I
don't think `CPS a` is the double negation.
But I can see how people can get confused. Given a value `x :: a` we can
embed it onto `CPS a` via `return x`. As we saw before we can pass from
`CPS a` to `DoubleNeg a`. So we have *two* ways for passing from `a` to
`DoubleNeg a`, the first one is directly as in the previous mail. The
second one is using `proof_CPS_DoubleNeg`
embed_onto_DoubleNeg :: a -> DoubleNeg
embed_onto_DoubleNeg = proof_CPS_DoubleNeg . return
where
return :: a -> CPS a
return a = ($ a)
So CPS is /almost/ the double negation. It is still interesting because
it's enough to embed a classical fragment of logic onto the constructive
fragment (LEM, pierce etc). But calling it a double negation really
tripped me off.
Am I correct? Or is there other reason why CPS is called the double
negation transformation?
Thank for your time reading this, I know it was long.
[1]: http://jelv.is/talks/curry-howard.html#slide30
[2]:
https://www.quora.com/What-is-continuation-passing-style-in-functional-programming
--
-- RubĂ©n
-- pgp: 4EE9 28F7 932E F4AD
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20200515/2dc9bd77/attachment.sig>
More information about the Haskell-Cafe
mailing list