1
$\begingroup$

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.

​​

$\endgroup$
1
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
0
$\begingroup$

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?

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – greybeard Aug 9 at 1:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.