Is having a `(a -> b) -> b` equivalent to having an `a`?

Question

In a pure functional language, the only thing you can do with a value is apply a function to it.

In other words, if you want to do anything interesting with a value of type a you need a function (for example) with type f :: a -> b and then apply it. If someone hands you (flip apply) a with type (a -> b) -> b, is that a suitable replacement for a?

And what would you call something with type (a -> b) -> b? Seeing as it appears to be a stand-in for an a, I'd be tempted to call it a proxy, or something from http://www.thesaurus.com/browse/proxy.

Answer 1

luqui's answer is excellent but I'm going to offer another explanation of forall b. (a -> b) -> b === a for a couple reasons: First, because I think the generalization to Codensity is a bit overenthusiastic. And second, because it's an opportunity to tie a bunch of interesting things together. Onwards!

z5h's Magic Box

Imagine that someone flipped a coin and then put it in a magic box. You can't see inside the box but if you choose a type b and pass the box a function with the type Bool -> b, the box will spit out a b. What can we learn about this box without looking inside it? Can we learn what the state of the coin is? Can we learn what mechanism the box uses to produce the b? As it turns out, we can do both.

We can define the box as a rank 2 function of type Box Bool where

type Box a = forall b. (a -> b) -> b

(Here, the rank 2 type means that the box maker chooses a and the box user chooses b.)

We put the a in the box and then we close the box, creating... a closure.

-- Put the a in the box.
box :: a -> Box a
box a f = f a

For example, box True. Partial application is just a clever way to create closures!

Now, is the coin heads or tails? Since I, the box user, am allowed to choose b, I can choose Bool and pass in a function Bool -> Bool. If I choose id :: Bool -> Bool then the question is: will the box spit out the value it contains? The answer is that the box will either spit out the value it contains or it will spit out nonsense (a bottom value like undefined). In other words, if you get an answer then that answer must be correct.

-- Get the a out of the box.
unbox :: Box a -> a
unbox f = f id

Because we can't generate arbitrary values in Haskell, the only sensical thing the box can do is apply the given function to the value it is hiding. This is a consequence of parametric polymorphism, also known as parametricity.

Now, to show that Box a is isomorphic to a, we need to prove two things about boxing and unboxing. We need to prove that you get out what you put in and that you can put in what you get out.

unbox . box = id
box . unbox = id

I'll do the first one and leave the second as an exercise for the reader.

  unbox . box
= {- definition of (.) -}
  \b -> unbox (box b)
= {- definition of unbox and (f a) b = f a b -}
  \b -> box b id
= {- definition of box -}
  \b -> id b
= {- definition of id -}
  \b -> b
= {- definition of id, backwards -}
  id

(If these proofs seem rather trivial, that's because all (total) polymorphic functions in Haskell are natural transformations and what we're proving here is naturality. Parametricity once again provides us with theorems for low, low prices!)

As an aside and another exercise for the reader, why can't I actually define rebox with (.)?

rebox = box . unbox

Why do I have to inline the definition of (.) myself like some sort of cave person?

rebox :: Box a -> Box a
rebox f = box (unbox f)

(Hint: what are the types of box, unbox, and (.)?)

Identity and Codensity and Yoneda, Oh My!

Now, how can we generalize Box? luqui uses Codensity: both bs are generalized by an arbitrary type constructor which we will call f. This is the Codensity transform of f a.

type CodenseBox f a = forall b. (a -> f b) -> f b

If we fix f ~ Identity then we get back Box. However, there's another option: we can hit only the return type with f:

type YonedaBox f a = forall b. (a -> b) -> f b

(I've sort of given away the game here with this name but we'll come back to that.) We can also fix f ~ Identity here to recover Box, but we let the box user pass in a normal function rather than a Kleisli arrow. To understand what we're generalizing, let's look again at the definition of box:

box a f = f a

Well, this is just flip ($), isn't it? And it turns out that our other two boxes are built by generalizing ($): CodenseBox is a partially applied, flipped monadic bind and YonedaBox is a partially applied flip fmap. (This also explains why Codensity f is a Monad and Yoneda f is a Functor for any choice of f: The only way to create one is by closing over a bind or fmap, respectively.) Furthermore, both of these esoteric category theory concepts are really generalizations of a concept that is familiar to many working programmers: the CPS transform!

In other words, YonedaBox is the Yoneda Embedding and the properly abstracted box/unbox laws for YonedaBox are the proof of the Yoneda Lemma!

TL;DR:

forall b. (a -> b) -> b === a is an instance of the Yoneda Lemma.

Answer 2

This question is a window into a number of deeper concepts.

First, note there is an ambiguity in this question. Do we mean the type forall b. (a -> b) -> b, such that we can instantiate b with whatever type we like, or do we mean (a -> b) -> b for some specific b that we cannot choose.

We can formalize this distinction in Haskell thus:

newtype Cont b a = Cont ((a -> b) -> b)
newtype Cod a    = Cod (forall b. (a -> b) -> b)

Here we see some vocabulary. The first type is the Cont monad, the second is CodensityIdentity, though my familiarity with the latter term isn't strong enough to say what you should call that in English.

Cont b a can't be equivalent to a unless a -> b can hold at least as much information as a (see Dan Robertson's comment below). So, for example, notice that you can never get anything out of ContVoida.

Cod a is equivalent to a. To see this it is enough to witness the isomorphism:

toCod :: a -> Cod a
fromCod :: Cod a -> a

whose implementations I'll leave as an exercise. If you want to really do it up, you can try to prove that this pair really is an isomorphism. fromCod . toCod = id is easy, but toCod . fromCod = id requires the free theorem for Cod.

Answer 3

The other answers have done a great job describing the relationship between the types forall b . (a -> b) -> b and a but I'd like to point out one caveat because it leads to some interesting open questions that I have been working on.

Technically, forall b . (a -> b) -> b and a are not isomorphic in a langauge like Haskell which (1) allows you to write an expression that doesn't terminate and (2) is either call-by-value (strict) or contains seq. My point here is not to be nitpicky or show that parametricity is weakened in Haskell (as is well-known) but that there may be neat ways to strengthen it and in some sense reclaim isomorphisms like this one.

There are some terms of type forall b . (a -> b) -> b that cannot be expressed as an a. To see why, let's start by looking at the proof Rein left as an exercise, box . unbox = id. It turns out this proof is actually more interesting than the one in his answer, as it relies on parametricity in a crucial way.

box . unbox
= {- definition of (.) -}
  \m -> box (unbox m)
= {- definition of box -}
  \m f -> f (unbox m)
= {- definition of unbox -}
  \m f -> f (m id)
= {- free theorem: f (m id) = m f -}
  \m f -> m f
= {- eta: (\f -> m f) = m -}
  \m -> m
= {- definition of id, backwards -}
  id

The interesting step, where parametricity comes into play, is applying the free theorem f (m id) = m f. This property is a consequence of forall b . (a -> b) -> b, the type of m. If we think of m as a box with an underlying value of type a inside, then the only thing m can do with its argument is apply it to this underlying value and return the result. On the left side, this means that f (m id) extracts the underlying value from the box, and passes it to f. On the right, this means that m applies f directly to the underlying value.

Unfortunately, this reasoning doesn't quite hold when we have terms like the m and f below.

m :: (Bool -> b) -> b
m k = seq (k true) (k false)

f :: Bool -> Int
f x = if x then ⊥ else 2`

Recall we wanted to show f (m id) = m f

f (m id)
= {- definition f -}
  if (m id) then ⊥ else 2
= {- definition of m -}
  if (seq (id true) (id false)) then ⊥ else 2
= {- definition of id -}
  if (seq true (id false)) then ⊥ else 2
= {- definition of seq -}
  if (id false) then ⊥ else 2
= {- definition of id -}
  if false then ⊥ else 2
= {- definition of if -}
  2

m f
= {- definition of m -}
  seq (f true) (f false)
= {- definition of f -}
  seq (if true then ⊥ else 2) (f false)
= {- definition of if -}
  seq ⊥ (f false)
= {- definition of seq -}
  ⊥

Clearly 2 is not equal to ⊥ so we have lost our free theorem and the isomorphism between a and (a -> b) -> b with it. But what happened, exactly? Essentially, m isn't just a nicely behaved box because it applies its argument to two different underlying values (and uses seq to ensure both of these applications are actually evaluated), which we can observe by passing in a continuation that terminates on one of these underlying values, but not the other. In other words, m id = false isn't really a faithful representation of m as a Bool because it 'forgets' the fact that m calls its input with both true and false.

The problem is a result of the interaction between three things:

1. The presence of nontermination.
2. The presence of seq.
3. The fact that terms of type forall b . (a -> b) -> b may apply their input multiple times.

There isn't much hope of getting around points 1 or 2. Linear types may give us an opportunity to combat the third issue, though. A linear function of type a ⊸ b is a function from type a to type b which must use its input exactly once. If we require m to have the type forall b . (a -> b) ⊸ b, then this rules out our counterexample to the free theorem and should let us show an isomorphism between a and forall b . (a -> b) ⊸ b even in the presence of nontermination and seq.

This is really cool! It shows that linearity has the ability to 'rescue' interesting properties by taming effects that can make true equational reasoning difficult.

One big issue remains, though. We don't yet have techniques to prove the free theorem we need for the type forall b . (a -> b) ⊸ b. It turns out current logical relations (the tools we normally use to do such proofs) haven't been designed to take into account linearity in the way that is needed. This problem has implications for establishing correctness for compilers that do CPS translations.