One may represent λ-terms in the λ-calculus using the following data type:
data LTerm a = Var a | App (LTerm a) (LTerm a) | Abs a (LTerm a)Describe the encoding of the constructors, the fold, the map and the case for this datatype.
The way I encoded constructors are:
Var x := λabc.ax
App t1 t2 := λabc.b (t1 abc) (t2 abc)
Abs x t := λabc.cx(t abc)
fold a b c d = d a b c
Can you help me to understand how to implement the map and the case in λ-calculus?
An example for map and case is the List datatype:
Nil = λnc.n
Cons a l = λnc.ca(lnc)
FoldList vgl = lvg
MapList f l = FoldList Nil (λaz.Cons (f a)z) l
$$ \text{case } l \text{ of} \begin{cases} \mathsf{Nil} \mapsto t_1 \\ \mathsf{Cons} \ a \ as \mapsto t_2 \end{cases} := \mathsf{CaseList} \ l \ t_1 \ (\lambda \ a \ as . t_2) $$
$$ \mathsf{CaseList} \ l \ t \ f := \pi_1 \left ( \mathsf{FoldList} \ \langle \mathsf{Nil}, \ t \rangle \ (\lambda \ a \ \langle l, \_ \rangle . \langle \mathsf{Cons} \ a \ l, \ f \ a \ l \rangle ) \ l \right ) $$
Thank you in advance.