Rank 3 Types function example

Question

I have this Rank 3 Type function definition:

f3 :: ((forall a. a -> a) -> Int) -> Bool -> Bool
f3 .... = ?

and I am struggling to write a simple example for it. Can you help?

Something slightly more complicated, possibly with all the parameters defined. — Randomize
Here is the thing: forall a. a -> a has only one (non-diverging) member: id. Then, there isn't anything interesting to do with the argument in (forall a. a -> a) -> Int - you already know it can only be id, so (forall a. a -> a) -> Int has to be some constant function. There is a bijection between the interesting (non-diverging) implementations of f3 and implementations of f3' :: Int -> Bool -> Bool. — Alec
Yes, you are right. Indeed I was not able to pass a meaningful parameter to it unless using some constant as you said. How can I change the signature to something more interesting? Replacing Int with a generic b I guess? and then eventually passing b as Bool and do a simple && with the other Bool parameter right? — Randomize

chi chi · Accepted Answer · 2017-02-01T09:57:40

f3 :: ((forall a. a -> a) -> Int) -> Bool -> Bool
f3 f b = (f id == 3) && b

f3_ex :: Bool
f3_ex = f3 f True where
   f :: (forall a. a -> a) -> Int
   f g = g 3

Changing the type to be more interesting, as mentioned in the comments:

f4 :: ((forall a. a -> a -> a) -> Int) -> Bool -> Bool
f4 f b = (f const == 3) && b

f4_ex :: Bool
f4_ex = f4 f True where
   f :: (forall a. a -> a -> a) -> Int
   f g = g 3 5


f5 :: ((forall a. a -> a -> a) -> Int) -> Bool -> Bool
f5 f b = f (if b then const else const id) == 42

f5_ex :: Bool
f5_ex = f5 f True where
   f :: (forall a. a -> a -> a) -> Int
   f g = g 3 5 + 39

Here f is essentially of type (Int, Int), the first component given by f const and the other one given by f (const id) or equivalently f (flip const).

Rank 3 Types function example

1 Answers