Lambda Expressions for Higher Order Function in Haskell

Question

Following this book, everything in Haskell is λ-calculus: A function like f(x)=x+1 can be written in Haskell as f = \x -> x+1 and , in λ expression as λx.x+1.

• What is λ expression for a higher order function like map::(a -> b) -> [a] -> [b]? Or λ expression for the function ($) :: (a -> b) -> a -> b?
• What about the list of functions (ie. f::[a->b])? A specific example can be h = map (\f x -> f x 5) [(-),(+)]. Then λ notation is something like h = map (λfx.f(x(5)) [(λab.a-b),(λab.a+b)]?

I'm just familiar with processes like alpha conversion, beta reduction but if you break down the function list in λ terms, that would be appreciated and no need of simplification.

Thanks.

Answer 1

First off,

everything in Haskell is λ-calculus

This is not really correct. Haskell has lots of features that don't correspond to something in untyped λ-calculus. Maybe they mean it could be compiled to λ-calculus, but that's kind of obvious, what with “any Turing-complete language...” jadda jadda.

What is λ expression for a higher order function like map :: (a -> b) -> [a] -> [b]

There are two unrelated issues here. The “higher order function” part is no problem at all for a direct λ translation, and as the comments already said

($) = \f -> \x -> f x   -- λf.λx.fx

or alternatively

($) = \f x -> f x
($) = \f -> f  -- by η-reduction

(which in Haskell we would further shorten to ($) = id).

The other thing is that map is a recursive function defined on an algebraic data type, and translating that to untyped λ-calculus would lead us quite far away from Haskell. It is more instructive to translate it to a λ-flavour that includes pattern matching (case) and let-bindings, which is indeed essentially what GHC does when compiling a program. It's easy enough to come up with

map = \f l -> case l of
               [] -> []
               (x:xs) -> f x : map f xs

...or to avoid recursing on a top-level binding

map = \f -> let go l = case l of
                        [] -> []
                        (x:xs) -> f x : go xs
            in go

We can't get rid of the let just like that, since λ-calculus doesn't directly support recursion. But recursion can also be expressed with a fixpoint combinator; unlike in untyped λ-calculus, we can't define the Y-combinator ourselves but we can just assume fix :: (a -> a) -> a as a primitive. That turns out to fulfill almost exactly the same job as a recursive let-binding, which is then immediately evaluated:

map = \f -> fix ( \go l -> case l of
                            [] -> []
                            (x:xs) -> f x : go xs )

To make up a λ-style syntax for this,

map = λf.fix(λg.λl.{l? []⟼[]; (x:s)⟼fx:gs})