Take

take is a general aggregator over a data set that returns the first $n$ items of a list.

Lambda Calculus

Take can be expressed in lambda calculus as a RANGE function where parameter s is 0 and e is the amount of items to retrieve from a list:

$\begin{eqnarray*} \lfunc{RANGE} := \llambda se. \lfunc{Y} (\llambda gc. \lfunc{LEQ}c e (\lfunc{PAIR} c (g (\lfunc{SUCC} c) e)) \lfunc{NIL} ) s \end{eqnarray*}$

using the following definitions:

$\begin{eqnarray*} \lfunc{Y} &:=& \llambda g. (\llambda x. g (x x)) (\llambda x. g (x x)) \\ \lfunc{LEQ} &:=& \llambda mn.\lfunc{ISZERO} (\boldmath\mathrm{SUB}\; m n) \\ \lfunc{ISZERO} &:=& \llambda n. n (\llambda x. \lfunc{FALSE}) \lfunc{TRUE} \\ \lfunc{FALSE} &:=& \llambda xy. y \equiv 0 \\ \lfunc{TRUE} &:=& \llambda xy.y \equiv K \\ \lfunc{SUB} &:=& \llambda mn. n \lfunc{PRED} m \\ \lfunc{PRED} &:=& \llambda nfx. n (\llambda gh. h (g f)) (\llambda u. x) (\llambda u. u) \\ \lfunc{PAIR} &:=& \llambda xyf. f x y \\ \lfunc{SUCC} &:=& \llambda nfx. f (n f x) \\ \lfunc{NIL} &:=& \llambda x. \lfunc{TRUE} \end{eqnarray*}$