# Lambda Calculus Conversion

How can I take a Haskell data type or function (eg fold, list, String, zip) and convert or translate it to a lambda calculus abstraction? Example: If sum computes a sum of all elements in a list, and :type sum = Num a => [a] -> a.

    sum []     = 0
sum (x:xs) = x + sum xs


How do I take this information to translate it to a lambda calculus expression, or rather an abstraction?

I have tried to find guides online but they just give me the answers. I want to know how to actually make the conversion/translation from a Haskell function like add, sum, map, fold, etc. to a lambda calculus abstraction.

​​

## 2 Answers

The thing to notice here is that your function sum is defined on lists, which are inductively defined. Theoretically, the inductive definition of a list defines for every type T a term

match_list :: T -> (a -> [a] -> T) -> ([a] -> T)


satisfying the property

match_list s t [] = s
match_list s t (x::xs) = (t x xs)


in addition, defining a recursive function requires an untypable fixed-point combinator fix satisfying the property

fix F = F (fix F)


so combining the two, we could write your definition by first defining

F :: ([a] -> a) -> ([a] -> a)
F := λ f -> match_list 0 (λ x -> (λ xs -> x + f xs))


and then

sum := λ x -> (fix F) x
= λ x -> (fix (λ f -> match_list 0 (λ x -> (λ xs -> x + f xs)))) x


To convince oneself that this works, let's try this on the example

sum [1,2] = (fix F) [1,2]
= (F (fix F)) [1,2]
= (λ f -> match_list 0 (λ x -> (λ xs -> x + f xs))) (fix F) [1,2]
= match_list 0 (λ x -> (λ xs -> x + ((fix F) xs))) [1,2]
= 2 + ((fix F) [1])
= 2 + ((F (fix F)) [1])
= 2 + ((λ f -> match_list 0 (λ x -> (λ xs -> x + f xs))) (fix F) [1])
= 2 + (match_list 0 (λ x -> (λ xs -> x + ((fix F) xs))) [1])
= 2 + (1 + ((fix F) []))
= 2 + 1 + ((F (fix F)) [])
= 2 + 1 + ((λ f -> match_list 0 (λ x -> (λ xs -> x + f xs))) (fix F) [])
= 2 + 1 + (match_list 0 (λ x -> (λ xs -> x + (fix F) xs)) [])
= 2 + 1 + 0


This is theoretically what would go on in a purely functional language (for example the untyped lambda calculus), however in languages like haskell, lisp, or ocaml (I am unaware of inductive datatypes in python), the terms match_list and fix are "internal" constructs and are not explicit terms in the language.

Try this.... It should help build up the intuition step by step

http://pages.cs.wisc.edu/~horwitz/CS704-NOTES/2.LAMBDA-CALCULUS-PART2.html

Alternatively since it's not really clear what you mean, maybe an example of what kind of abstraction you want for something simpler than sum?

• Welcome to COMPUTERSCIENCE @SE. I concede that you are not in a position to provide that hyperlink as a comment to the question. Please (re)visit How do I write a Good Answer? – greybeard Aug 9 at 1:24