No, although you do see that in set theory, but this is a specific idea about the type signatures and encodings.
List type:
type Stack<x> = null | {first: x, rest: Stack<x>}
The church encoding of a data structure, is to go through all of these cases separated by |, and define a handler for each one, and then define a function which accepts all those handlers and calls the appropriate one for its case:
type StackF<x> = <z>(
ifNull: (n: null) => z,
ifItem: (first: x, rest: z) => z
) => z;
The Scott encoding is actually a little more practical, and has `rest: StackF<x>` in that second handler, but that's not what we have here.
Now the point is that a unit type like `null` that only has one possible value, that first handler can actually be simplified to just `ifNull: z`. Similarly if we consider a list of nulls, we would get
type NullStackF = <z>(
ifEnd: z,
ifItem: (rest: z) => z
) => z;
And after swapping the arguments and currying, you get precisely the type of the Church numerals.
The Church encoding of a list is effectively replacing that list with its reduce function, so that's why I am saying that it's basically Array prototype.reduce on an Array<null> type. (I actually think it's reduceRight but this type is symmetric under .reverse() so who gives a darn). So it's
const zero_ = f => [].reduce(f)
const one_ = f => [null].reduce(f)
const two_ = f => [null, null].reduce(f)
in JS. But if you had just Scott-encoded the numbers instead, you would have had no problems with pred() but you need the Y combinator to actually use the numerals for something interesting:
type ScottNum = <z>(next: (rest: ScottNum) => z) => (z: z) => z;
const zero: ScottNum = _f => x => x
const one: ScottNum = f => _x => f(zero)
const two: ScottNum = f => _x => f(one)
function succ(n: ScottNum): ScottNum {
return f => _x => f(n)
}
function pred(n: ScottNum): ScottNum {
return n((x: ScottNum) => x)(zero)
}
function church<z>(n: ScottNum, f: (z: z) => z): (z: z) => z {
return z => n(m => f(church(m, f)(z)))(z)
}
List type:
The church encoding of a data structure, is to go through all of these cases separated by |, and define a handler for each one, and then define a function which accepts all those handlers and calls the appropriate one for its case: The Scott encoding is actually a little more practical, and has `rest: StackF<x>` in that second handler, but that's not what we have here.Now the point is that a unit type like `null` that only has one possible value, that first handler can actually be simplified to just `ifNull: z`. Similarly if we consider a list of nulls, we would get
And after swapping the arguments and currying, you get precisely the type of the Church numerals.The Church encoding of a list is effectively replacing that list with its reduce function, so that's why I am saying that it's basically Array prototype.reduce on an Array<null> type. (I actually think it's reduceRight but this type is symmetric under .reverse() so who gives a darn). So it's
in JS. But if you had just Scott-encoded the numbers instead, you would have had no problems with pred() but you need the Y combinator to actually use the numerals for something interesting: