haskellrank-n-types

Rank 3 Types function example


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?


Solution

  • 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).