How to come up with rank N type functional description of data types?

Question

In our functional programming lecture we are told that we can express the  boolean type as functions as the following:

type Boolean = ∀a . a → a → a

In a similar fashion we can express the naturals by

type Natural = ∀a . (a → a) → (a → a).

or lists by

newtype ChurchList a = CL (∀b.(a → b → b) → b → b).

My question is, how does one come up with such a translation of a datatype into a function? Is there a systematic way or algorithm to do this ? Why does this always work and what is the intuition behind this ?

Answer 1

I am not sure whether the following comment points in the right direction. Anyway, have a look at https://en.wikipedia.org/wiki/Church_encoding and Barendregt's book as well as his article in the handbook of logic in computer science.

In general, one can introduce new types as an abbreviation of an existing set of other types in the type universe. Of course, there are many ways how this can be done. In higher order logic theorem provers that is usually done by such a type together with two functions that translate the new type into the available one and back. That is defined in more detail in Tom Melham's paper:

T. Melham, ‘Automating Recursive Type Definitions in Higher Order Logic’, in Current Trends in Hardware Verification and Automated Theorem Proving, edited by G. Birtwistle and P. A. Subrahmanyam (Springer-Verlag, 1989), pp. 341–386.

It is clearly required that the two sets in question have the same cardinality which gives you a first hint on how to select a suitable set. In that way, all types like booleans, natural numbers, integers, lists, sets, reals, etc. are defined on top of a basic set of individuals which is an unspecified infinite type that builds up the semantic universe of a higher order logic. Again Melham's paper above shows some of these constructions.

For primitive recursive types, there is a recipe for a type definition. Melham's achievement was to automate the definition of primitive recursive types in higher order logic which you can find in the above paper so that users of the theorem prover just have to list the primitive recursive definition, and Melham's procedure automatically implemented its embedding in the existing types.

Note that once you have natural numbers, Gödelization allows one to embed also other data types. That is typically not comfortable, so that is why Melham's work abstracts from that and introduces new types. Church initiated such encodings that are nowadays also used in higher order logic theorem provers.  

Answer 2

In the simple case, if you have a datatype with "n" constructors, the type will have the form "∀a . C_1 -> C_2 -> ... -> C_n -> a".

For example, as a list has constructors "Cons" and "Nil", you will have the form "∀b . CaseCons -> CaseNil -> b".

Each "C_i" is a function type, where the arguments are the parameters of the constructor. If the parameter contains a recursive occurrence of the datatype, it is replaced by the result (or results) for computing the recursive case(s).

For example, the list constructor "Cons :: a -> List a -> List a" means that the function "CaseCons" above has the form "a -> b -> b".

The Nil constructor has no parameters, so "CaseNil" will be just "a".

The construction is a bit more complicated for mutually recursive datatypes or when the defined type does appear nested within another datatype (e.g. a tree where a node has a list of children).
For mutual recursion, you can use more than one universally quantified variables (one per datatype).
Nested recursion can be transformed to a mutually recursive definition.

I think there are also cases, where the construction is not possible. At least I would not know how to do it for something like "data X = A (X -> Bool) | B".