Odtnhj

I have the following definition for a function in Haskell.

> q7 :: forall a. forall b. ((a -> b) -> a) -> a

I am challenged to either create a definition for it, or state why a definition does not exist. Here are my thoughts:

q7 takes in any types for a and b. The statement (a -> b) -> a would be implemented by taking two items and returning the latter. Now, if I go one tier further, I can just return this same "a" to fulfill ((a -> b) -> a) -> a. I see an issue in that a and b can be any type, so for each instance of a, could a be a different type? For example, could it be something like ((Int -> Bool) -> [Char]) -> Int? I probably murdered that syntax. If anyone has any hints or if anyone can confirm or deny my ideas, I would appreciate it greatly!

It's impossible, except by using infinite recursion or runtime errors, so to fail to terminate.

We can prove that it is indeed impossible, exploiting some results from theoretical computer science. I don't know if there's an easier way to show that it's indeed impossible.

If there were a way to write a terminating program with that type, by the Curry-Howard correspondence, we would get that the logical formula ((a -> b) -> a) -> a (here, read -> as "implies") is a theorem of propositional intuitionistic logic.

Such formula is known as Peirce's Law, and is one of the key examples of a formula which is NOT provable in intuitionistic logic (by constrast, it is a theorem in classical logic).

As a reasonably easy way to prove that Peirce's law is not an intuitionistic theorem, one can run a decision procedure for propositional intuitionistic logic, and observe that it outputs "not a theorem". As such procedure, we could perform a search for a cut-free proof in Gentzen's LJ sequent calculus: in this way we only need to check a finite (and smallish) number of possible proofs, and observe that each attempt fails.

Suppose you have a function

pierce :: ((a -> b) -> a) -> a

Import

data Void

from Data.Void.

Now we get to play games. We can instantiate a and b in the type of pierce to whatever we like. Let's define

type A p = Either p (p -> Void)

and instantiate with

a ~ A p
b ~ Void

So

pierce :: ((A p -> Void) -> A p) -> A p

Let's write a helper:

noNegate :: forall p r. (A p -> Void) -> r
noNegate apv = absurd (n m)
 where
 m :: p -> Void
 m = apv . Left

 n :: (p -> Void) -> Void
 n = apv . Right

Now we can go for the kill:

lem :: Either p (p -> Void)
lem = pierce noNegate

If this function existed, it would be very strange.

lem @Void = Right id
lem @() = Left ()
lem @Int = Left ... -- some integer, somehow

The behavior of this function seems so weird because it violates parametricity, which Haskell functions can't do, but things only get worse for it.

It's possible (but slightly annoying) to encode an arbitrary Turing machine as a Haskell type. And it's possible to design a type representing a proof that a particular Turing machine will halt (basically a type-indexed execution trace). Applying lem at such a trace type would solve the halting problem.

Thanks to Haskell's laziness, some "impossible" functions turn out to be useful, albeit partial. For example,

fix :: (a -> a) -> a

is formally absurd, since fix id claims to give you anything you want. pierce is not such a function. Let's try to write it:

pierce :: ((a -> b) -> a) -> a
pierce f = _

What must go on the right side? The only way to make an a is by applying f.

pierce f = f _

We must now supply something of type a -> b. We don't have one. We don't know what b is, so we can't pull the usual trick of starting with some b constructor to gain a beat. Nothing can ever improve our b. So the very best we can do is

pierce f = f (const undefined)

which doesn't look remotely useful.

The statement (a -> b) -> a would be implemented by taking two items and returning the latter.

You're confusing this with a -> b -> a (which can also be written a -> (b -> a). This is not the same.

(a -> b) -> a is a function that takes a single argument and returns a value of type a. The argument has type a -> b, which means it is a function that takes a value of type a and returns a value of type b. This is not unlike (for example) the filter function:

filter :: (a -> Bool) -> [a] -> [a]

This takes two arguments, a predicate function of type a -> Bool and a list of type [a], and returns a new filtered [a] value by passing each list item to the predicate.

I see an issue in that a and b can be any type, so for each instance of a, could a be a different type?

No, if it could it would have a different name. a can be any type, but once you pick a type for a, every a in that type signature stands for that type. The b is a different letter, so it can be a different type from a.

So, for your type signature ((a -> b) -> a) -> a, you would write a function that takes a single argument (another function) and returns an a. The argument function has type (a -> b) -> a, which means it takes a function of type a -> b as an argument and returns an a.

func :: ((a -> b) -> a) -> a
func f = ...

The argument f, if called, would return an a that you could then return from func:

func :: ((a -> b) -> a) -> a
func f = f x
 where x :: a -> b
 x = ...

However, to call f you would need to pass it a function a -> b, for all types a and b. As you don't have such a function available, and there's no way to write such a function in general, I think this is impossible to implement.