On an automatic translation of typed lambda calculus in untyped lambda calculus I have a question regarding the "compilation" of typed lambda calculus in untyped lambda calculus.
Take for example the inductive definition of lists, with introduction rules:

and:

We can automatically derive the elimination rule and the computation rules (here
omitted as they are well known), as well as an interpretation in untyped lambda
calculus:
$[\![Nil]\!] = \lambda x.\lambda y.x$
$[\![Cons(a,l)]\!] = \lambda x.\lambda y.y \> [\![a]\!] \> ([\![l]\!] \> x \> y)$
$[\![ListCata(l,n,c)]\!] = [\![l]\!] \>[\![n]\!] \> [\![c]\!]$
This "automatic definition" can be done, up to my knowledge, if we are
defining an inductive type $I$ such that the occurrences of $I$ in the premises
of the introduction rules are strictly positive.
It seems to me that the power of this method
lies in his generality: I only have to state my introduction rules and I automatically get a translation in a language I know how to execute, in this case untyped lambda calculus.
Now, I'm interested in a better understanding of this type of translation, in different directions:


*

*Where has this schema been first defined? Are there papers regarding this
translation?

*What are the limits of this approach? For example, can I extend this
process to more inductive types, to co-inductive types, to a polymorphic
lambda calculus, to dependent types?

*What if I'd like, given a definition of an inductive type, "compile" the
code in, for example, SKI calculus, or another system of symbolic computation?
Is there any work done in this direction?

*Could one hope to give an inductive definition of the underlying "computational machine", and get automatically a translation?

 A: The translation process you describe is often referred to as the Church encoding, and it is rather well studied in the literature. Presumably it was first given by Church soon after the definition of the $\lambda$-calculus itself (some details appear here).
One way to see it is as a "control inversion", where an instance of pattern matching on an element of an inductive type simply becomes an application of each branch to the term.
This translation doesn't necessarily have to be to the untyped calculus: the usual Church encoding of (positive) data-types in System F results in well-typed terms! In general this extends to polymorphism and dependent types without difficulty, though the induction principles for those types can not be proven inside the type theories themselves! (See e.g. Geuvers for a proof).
The question about compiling to combinators seems unrelated. Of course it is possible to represent every $\lambda$-term using combinators, and using combinators as targets for compilation is another well studied subject (see e.g. Hudak & Kranz).
