Lambda calculus lists construction explanation

Question

I have the following notes that introduce how lambda calculus handles lists. They go as follows:

A list is something we can match on and deconstruct if it is not empty:

list match{
 case Nil => M
 case Cons(x,y) => N(x,y)
}

A list value is given by how it interacts with two terms M and N

(1) For starters I don't understand at all what is the role of M and N here. Then it continues:

We define it (a list) as a function that will take such M and N as arguments

$Nil = \lambda mn.m$

$Cons(P,Q) = \lambda mn. n (P,Q)$

(2) Assuming I know how pairs and if constructs work in lambda calculus how can I come up with this expressions myself? I suppose that once this is clear I will be able to understand this sentence:

Cons is like a pair but takes m as argument, too, to fit along with nil

Can you clarify points (1) and (2)?

Edit:

This are some further comments made in my notes that may make easier to understand what the intention of the writer is:

$Nil \ M \ N \implies M$ $Cons(P,Q) \ M \ (\lambda p. p._1) \implies \cdots \implies (P,Q)._1$

• Euge: I assume you forgot an end of line after the second $M$
• Euge: Can you figure out how to construct functions with this representation? Can you define, for example, the function $cons$? or $isNil$? or $head$? (assuming pairs and booleans). Trying to use lists is a very good way to unravel this.

Answer 1

There are several ways to define lists in lambda calculus. You can find them here.
Your definition doesn't seem to fit exactly in any of those (please, check that).
Anyway, I'll try to answer to your questions.

Lists (and many data types) can be defined in lambda calculus in terms of the way to deconstruct them.

If you are familiared with the fold operation, you know it follows this specification:

$fold\ Nil\ e\ f$ = $e$
$fold\ (Cons\ x\ l)\ e\ f$ = $f\ x\ (fold\ l\ e\ f)$

Many functions over lists can be defined with $fold$. For example, if you want to sum the elements of a list $l$ of integers, you can do:

$sum\ Nil = 0 $
$sum\ (Cons\ x\ l) = +\ x\ (sum\ l) = x + sum\ l$

Or just say:

$sum\ l = fold\ ,円 l\ 0\ +$

In this case, you can imagine that the $sum$ functions replaces the empty list with 0ドル$ and the cons operator with '+'.

So, if we want to define lists in lambda calculus, a way of doing it is to define each constructor ($Nil, Cons$) to do the work of $fold$.
The fist step is to state that $fold$ is just the identity function ($\lambda x . x$). Then we get the $fold$ specification to be our specification for $Nil$ and $Cons$:

($\lambda x . x$)$\ Nil\ e\ f$ = $e$
($\lambda x . x$)$\ (Cons\ x\ l)\ e\ f$ = $f\ x\ ((\lambda x . x)\ l\ e\ f)$

This is the same as:

$Nil\ e\ f$ = $e$
$(Cons\ x\ l)\ e\ f$ = $f\ x\ (l\ e\ f)$

Rewriting it a bit, we get:

$Nil$ = $\lambda e\ f.e$
$(Cons\ x\ l)$ = $\lambda\ e\ f. f\ x\ (l\ e\ f)$

So, this answers fits in the last form of definition of lists from the wiki (using right fold). But it is important to notice that is not the only way. The way you posted seems to do the same as here, but instead of using the $fold$ operator, using some sort of $destructor,ドル where:

$destructor\ Nil\ m\ n = m$
$destructor\ (Cons\ x\ l)\ m\ n = n\ x\ l$

• user1868607: Can you imagine what is the role of M and N and the meaning of the phrase: Cons is like a pair but takes m as argument, too, to fit along with nil?
• Euge: Where have you read that? I mean, which book do you follow? I agree is not pedagogical at all. I also don't know how they define pairs, but it can be done following the methodology I just exposed. Regarding, M and N, you can check the definition of $destructor$ above. They are just place holders for what a function over list should do. You start with a way to destruct lists and from that, you get a representation in lambda calculus, which is necessarily made with functions. Also, a good way to begin to understand this representations is to check church numerals.