[Haskell-cafe] Relationship between ((a -> Void) -> Void) and (forall r. (a -> r) -> r)

[Li-yao Xia]

Hi Ruben,

 > 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

You're reading too much into this claim. When I read "CPS", I would 
think of types of the form ((a -> r) -> r), but how the r gets 
instantiated or quantified is very context-dependent.

Note that (forall r. (a -> r) -> r) is isomorphic to a. From that, you 
can conclude that it is not isomorphic to ((a -> Void) -> Void).

Looking at types only, the correspondence between double negation and 
CPS is only a superficial observation that ((a -> Void) -> Void) matches 
((a -> r) -> r) simply by setting (r = Void). But CPS is a program 
transformation before all. Therefore, to understand the correspondence 
with double negation, we should really be looking at the level of terms 
(programs or proofs).

1. Define a language of proofs in classical logic. Below is one of many 
ways of doing it, notably featuring a rule for double-negation 
elimination (NotNot). A term (x :: K a) is a proof of the proposition a.

data K a where
   AndI :: K a -> K b -> K (a :*: b)
   OrIL :: K a -> K (a :+: b)
   OrIR :: K b -> K (a :+: b)
   ImplI :: (a -> K b) -> K (a :->: b)
   Assumption :: a -> K a
   Cut :: K (a :->: b) -> K a -> K b
   NotNot :: K (Not (Not a)) -> K a

2. Double negation enables a translation of classical logic in 
intuitionistic logic, here embedded in Haskell:

translate :: K a -> Not (Not a)
translate (NotNot p) k =
   translate p \f ->
   f k
translate (Cut pf px) k =
   translate pf \f ->
   translate px \x ->
   f x k
{- etc. -}
{- also omitted: the translation of formulas ((:*:), (:+:), (:->:), Not) 
which is performed implicitly in the above definition of K. -}

Full gist: https://gist.github.com/Lysxia/d90afbe716163b03acf765a2e63062cd

The point is that the proof language K is literally a programming 
language (with sums, products, first-order functions, and a weird 
operator given by double negation elimination), and the "translate" 
function is literally an interpreter in the programming sense, which one 
might call a "shallowly embedded compiler", where the target language is 
in continuation-passing style.

Thus, CPS transformation and double-negation translation don't just look 
similar; when phrased in a certain way, they are literally the same thing.

The translation is not unique. There are multiple flavors of "CPS 
transformation" (or "double-negation translation") depending on where 
exactly negations are introduced in the translation of formulas.

Cheers,
Li-yao

On 5/15/20 5:19 AM, Ruben Astudillo wrote:
> 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
> 
> 
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
>