Lambda Calculus Conversion

Question

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.

​​

Answer 1

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.

Answer 2

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?