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.

CodePudding user response：

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 f     =     c
 -- a       :: a
 --   f g   ::    c
 --     g b :: a
  where
  c = f g
  g       b =  a

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

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.

See also.

CodePudding user response：

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)