Defining a function that satisfies a type in Haskell

Question

Considering the type

foo :: a -> ((b -> a) -> c) -> c

I want to create a function that satisfies this type...

I know foo x y = y (\z -> x) satisfies this type as confirmed with :type in GHCi, but how would I get to this final function manually, or step by step?

I also know foo2 f g = \x -> f (g x) would also satisfy foo2 :: (a -> b) -> (c -> a) -> c -> b but don't also know how to get to this function.

Answer 1

Question 1

foo :: a -> ((b -> a) -> c) -> c

says that foo has to take an a and a function with type (b -> a) -> c and somehow produce a c.

foo a function = c

where a::a and function::(b -> a) -> c but where can we get the c from?

Good news: function makes cs for us.

Let's use that. function::(b->a) -> c so we can get a c if we give it a (b->a).

So we need to first make a helper function that takes bs and gives us as:

foo a function = 
   let helper b = a

That's fine! I already had an a so I could use that. We just need to hand function the helper we just made:

foo :: a -> ((b -> a) -> c) -> c
foo a function = 
   let helper b = a 
   in function helper

Now notice that helper ignores its input, so we could write

foo :: a -> ((b -> a) -> c) -> c
foo a function = 
   let helper _ = a 
   in function helper

And we can use lambda notation for helper:

foo :: a -> ((b -> a) -> c) -> c
foo a function = 
   let helper = \_ -> a 
   in function helper

But now we could just write (\_ -> a) instead of helper:

foo :: a -> ((b -> a) -> c) -> c
foo a function = 
   function (\_ -> a)

And finally, lets abbreviate function as f:

foo :: a -> ((b -> a) -> c) -> c
foo a f = f (\_ -> a)

Question 2

foo2 :: (a -> b) -> (c -> a) -> c -> b

OK, this time we need to make a b. We're given a c and a couple of functions for turning as into bs and cs into as:

foo2 :: (a -> b) -> (c -> a) -> c -> b
foo2 
   make_b_from_a 
   make_a_from_c 
   c 
      = b

Well, the only thing that can give us a b is make_b_from_a:

foo2 :: (a -> b) -> (c -> a) -> c -> b
foo2 
   make_b_from_a 
   make_a_from_c 
   c 
      = make_b_from_a a

but now we need an a, but we can use make_a_from_c for that, and we already have a c:

foo2 :: (a -> b) -> (c -> a) -> c -> b
foo2 
   make_b_from_a 
   make_a_from_c 
   c 
      = make_b_from_a (make_a_from_c c)

Let's shorten the names. I'm going to call the (c->a) one f because we use it before the other one, which I'll call g:

foo2 :: (a -> b) -> (c -> a) -> c -> b
foo2 g f c = g (f c) 

We can take the last argument using a lambda:

foo2 :: (a -> b) -> (c -> a) -> c -> b
foo2 g f = \c -> g (f c) 

Answer 2

It's just a matter of fitting the matching pieces of a puzzle together. The same-named pieces match. The type of foo means it's a function with two parameters:

foo :: a -> ((b -> a) -> c) -> c
--     a    f

foo a f     =     c
 -- a       :: a
 --   f g   ::    c
 --     g b :: a
  where
  c = f g         -- produce a c-type value
  g       b =  a  -- define g to produce
                  --   the value a

f we're given, but g we must invent so that it returns a; fortunately, we're already given an a:

-- f :: ((b -> a) -> c)
--       g

-- g ::   b -> a

a is given to us as a parameter of foo, and b is just an unused parameter of g.

Next we can substitute and simplify, using the fact that writing this:

p :: q -> r
p    q =  r...

is the same as writing this:

p :: q -> r
p = \q -> r...

where we use r... to indicate an expression whose type is r.

Also, s -> t -> r is the same as s -> (t -> r) because, similarly,

h :: s ->   t -> r
h    s      t =  r...
h    s =  (\t -> r...)
h = \s -> (\t -> r...)

all express the same thing.

Your second question can be addressed in the same manner.

x :: a means "the value x has type a"; a :: a means "the value a has type a". The same name a can be used in two different roles; when you're accustomed to it, it can actually be quite a helpful mnemonic.

See also.

Answer 3

An underscore _, or an undefined name beginning with an underscore such as _what, is treated by GHC as a “hole” that you want to fill in. You can use this to ask what type the compiler is expecting, and this can be helpful in figuring out how to iteratively fill in the program. Thankfully, this is a case where it’s very helpful, so I can easily go through it step by step in GHCi (with > indicating the prompt). We begin with a hole foo = _:

> foo :: a -> ((b -> a) -> c) -> c; foo = _

And we receive a message saying Found hole: _ :: a -> ((b -> a) -> c) -> c. GHC suggests foo :: a -> ((b -> a) -> c) -> c as a valid way of filling in the hole, and indeed foo = foo is legal, it’s just not the answer we’re looking for, since it represents an infinite loop.

Instead, we can look at the type and break it down into parts from the top down. We begin with a function type (->) whose input is a and whose output is ((b -> a) -> c) -> c. We can make a function value using a lambda expression, inventing a name for the a value, say x, and put another hole for the body:

> foo :: a -> ((b -> a) -> c) -> c; foo = \ x -> _

…
    • Found hole: _ :: ((b -> a) -> c) -> c
…

It now mentions that we have x :: a available to work with, in addition to foo, but this isn’t quite enough, so next we can take apart ((b -> a) -> c) -> c into its input ((b -> a) -> c) and output c. (From now on, for brevity’s sake, I’ll also skip repeating the type signature of foo.)

> foo :: …; foo = \ x -> \ f -> _

…
    • Found hole: _ :: c
…

We can’t take apart the type variable c any further, and we know we need to make a value of type c, so we can look at what we have available:

• f :: (b -> a) -> c
• x :: a
• foo :: a -> ((b -> a) -> c) -> c

So our options are:

1. Recursively call foo

2. Call f

#1 would quickly put us back in the same situation we’re in, so #2 is all that’s left. f expects a value of type b -> a as an argument:

> foo :: …; foo = \ x -> \ f -> f _

…
    • Found hole: _ :: b -> a
…

So again we can write a lambda:

> foo :: …; foo = \ x -> \ f -> f (\ y -> _)

…
    • Found hole: _ :: a
…

The only way we can produce a value of the unknown type a is to use the value x :: a that we’ve been given, so the final result is this:

foo = \ x -> \ f -> f (\ y -> x)

And that can be written in exactly the same form as you put in your question, using a little syntactic sugar, and a couple different choices of variable names:

foo     = \ x -> \ f -> f (\ y -> x)
foo x   =        \ f -> f (\ y -> x)
foo x f =               f (\ y -> x)

foo x y =               y (\ z -> x)