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.

$ = \f -> \x -> f x becomes λf.λx.f(x). It's literally just a different syntax for the same thing. — Bergi
– Bergi, Commented Jun 3, 2020 at 12:27
Correct me if I'm wrong but when you write λf.λx.f(x), it means a function that returns f(x)? While ($) :: (a -> b) -> a -> b takes in a function λx. termsOf(x) and returns another function or λx. termsOf(x) ? — Tuan
– Tuan, Commented Jun 3, 2020 at 12:34
Abstract datatypes only predefine type constructors and destructors. In particular :: and [] is syntactic sugar for two constants cons :: α → [α] → [α] and nil :: [α]. The list [1,2,3] is just a term 1::2::3::[] or with even less syntactic sugar cons(1, cons(2, cons(3, nil))). — lambda.xy.x
– lambda.xy.x, Commented Jun 3, 2020 at 12:53
In untyped lambda calculus, a higher-order function is just a function, as you can't say anything about what any particular variable represents; everything is encoded in terms of how applications of abstractions relate to each other. Typed lambda calculus is another matter. — chepner
– chepner, Commented Jun 3, 2020 at 12:55

leftaroundabout · Accepted Answer · 2020-06-04 01:16:11Z

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

Will Ness · Accepted Answer · 2020-06-04 15:00:57Z

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

Collectives™ on Stack Overflow

Lambda Expressions for Higher Order Function in Haskell

2 Answers 2

Comments

Comments

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

2 Answers 2

Comments

Comments

Your Answer

Sign up or log in

Post as a guest

Related