CODEWITHSUNDEEP
haskellfunctional-programminghigher-order-functionslambda-calculus
Tuan
Tuan

Reputation: 94

Lambda Expressions for Higher Order Function in Haskell

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.

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.

Upvotes: 1

Views: 1085

Answers (2)

Will Ness
Will Ness

Reputation: 71065

(warning: the following code contains an error, leading to the definition which results in the equation map f (x:xs) == f x : map f (map f xs), as far as I can tell.)

Continuing on the answer by @leftaroundabout,

MAP = λf.Y(λg.λl.l(NIL)(λxs.CONS(fx)(gs)))

Y is a fixed-point combinator:

Y = λg.(λx.g(xx))(λx.g(xx))   -- Yg == g(Yg)

-- MAP(f) == (λl.l(NIL)(λxs.CONS(fx)(MAP(f)s)))

Lists are lambda terms that accept two arguments to be applied appropriately, first in case the list is empty, second if not:

-- constructs an empty list
NIL = λnc.n

-- constructs a non-empty list from its two constituent parts
CONS = λadnc.ca(dnc)

Thus e.g. a term returned by CONS(1)(CONS(2)NIL) will be transformed by MAP(f) to

MAP(f)(NIL)nc -> (NIL)nc -> n
MAP(f)(CONS(2)NIL)nc -> CONS(2)NIL(NIL)(λxs.CONS(fx)(MAP(f)s))nc
                     -> (λxs.CONS(fx)(MAP(f)s))(2)(NIL)nc
                     -> CONS(f(2))(MAP(f)(NIL))nc
                     -> c(f(2))(MAP(f)(NIL)nc)
                     -> c(f(2))((NIL)nc)
                     -> c(f(2))n
MAP(f)(CONS(1)(CONS(2)NIL))nc ->
                     -> CONS(1)(CONS(2)NIL)(NIL)(λxs.CONS(fx)(MAP(f)s))nc
                     -> (λxs.CONS(fx)(MAP(f)s))(1)(CONS(2)NIL)nc
                     -> CONS(f(1))(MAP(f)(CONS(2)NIL))nc
                     -> c(f(1))(MAP(f)(CONS(2)NIL)nc)
                     -> ....
                     -> c(f(1))(c(f(2))n)

Upvotes: 2

leftaroundabout
leftaroundabout

Reputation: 120711

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})

Upvotes: 3

Related Questions