I read many similar topics and still don't understand. So the question is to create a function that has a specific type for example given type Integer-> Integer a function that has that type is \x-> x 1 how to find a function given a type using lambda.

1. (((Int → a) → a) → b) → b
2. (a -> b) -> c
3. a → (a → a)
4. (b -> c) -> (a -> b) -> a -> c

i solved 4) by guessing

Three variables after lambda, f which has a type b->c, g has type a->b, and a :t \f g a -> f (g a) i don't really get the steps just that there inputs (b->c),(a->b) and a. then guessed the order

for 1) there is just one input so it should be \f-> \g->...

CodePudding user response：

One of the best ways to solve these exercises in practice is to use holes: write _ for a hole to be filled and read from GHCi about the type of that hole

> foo :: (((Int -> a) -> a) -> b) -> b ; foo = _
    * Found hole: _ :: (((Int -> a) -> a) -> b) -> b

The hole is a function. Let's use a lambda then.

> foo :: (((Int -> a) -> a) -> b) -> b ; foo = \f -> _
    * Found hole: _ :: b
    * Relevant bindings include
        f :: ((Int -> a) -> a) -> b

The hole must have type b. No more lambdas. We can't create a value of type b, unless we somehow apply f (note the printed type of f).

> foo :: (((Int -> a) -> a) -> b) -> b ; foo = \f -> f _
    * Found hole: _ :: (Int -> a) -> a

Ah, now the hole is a function again. Another lambda.

> foo :: (((Int -> a) -> a) -> b) -> b ; foo = \f -> f (\g -> _)
    * Found hole: _ :: a
    * Relevant bindings include
        g :: Int -> a

Well, now we need to produce a. With g :: Int -> a at our disposal it looks easy.

> foo :: (((Int -> a) -> a) -> b) -> b ; foo = \f -> f (\g -> g 42)

No more holes -- done.

Note that your 2) (a -> b) -> c is impossible to realize properly -- there is no way to produce a c from that input. You can only write non-terminating (or crashing) programs with that type.

CodePudding user response：

(b -> c) -> (a -> b) -> a -> c represents a function with 3 polymorphic parameters, first 2 parameters are also functions, first one is b -> c (function accepting b and returning c) and second one is a -> b (function accepting a and returning b) (see higher order functions). Lambda \f g a -> f (g a) has three parameters and is implemented by result of calling g with parameter a passed to f.