Abstract

Except adding built-in data types into the language, there are several encoding approaches to translate them into plain lambda terms. In this talk I will introduce the Church, Scott and Church-Scott encoding of data types. Although the encodings look similar, each of them has certain advantages and limitations. I will also demonstrate that by examples.