CODEWITHSUNDEEP
lambda-calculuschurch-encoding
MathuSum Mut
MathuSum Mut

Reputation: 2825

What is the purpose of Church Encoding?

Lately I was reading articles about Lambda calculus and Church Encoding, and although I formed a remote understanding of what they entail, I am having trouble finding purpose for using higher-order functions to represent numeric values or lists instead of using numeric values or lists directly.

In programming, performing Lambda calculus on Church-Encoded expressions is extremely taxing on the machine's resources, and just seems like a considerably less efficient technique of doing anything. I find that programmers usually consider it bad programming practice, except from Scheme or Haskell programmers, for odd reasons.

Is there any actual practical reason to use Church encoding? Or is it only useful in theoretical study?

Upvotes: 2

Views: 730

Answers (2)

winitzki
winitzki

Reputation: 3347

There is one practical use of Church encodings that has come up recently. The use case is the programmable configuration language called Dhall. In that language, recursion is not allowed, but the language includes all of System F and a bit more. So, Church encoding is possible and is the official way of using recursive data types (e.g., trees, to represent JSON data) in Dhall.

What practical advantages does this bring? Because Church encoding guarantees termination (you cannot ever make an infinite loop), the Dhall language can use the Church encoding to represent some recursive types and code while fully preserving its strong normalization property and guaranteed termination. (Configuration files are guaranteed to never have infinite loops.)

Upvotes: 0

Cactus
Cactus

Reputation: 27636

Analysis of a (formal) language becomes technically simpler the smaller it is. If you can represent, for example, data types as functions (which is what the Church encoding gives you), then you don't need to add data types to your language just to be able to examine how you can manipulate data in it.

For a practical programming language, yes, you most often add bespoke data type support; but you can still define their semantics by reducing them to functions and then using just the semantics of the smaller, data type-less language.

Upvotes: 5

Related Questions