Church encodings and naturality

Fredrik Nordvall Forsberg

(University of Strathclyde)

Church encodings can be used to construct weakly initial algebras in
impredicative type systems such as System F or the Calculus of
Constructions. In the latter, we can also ask whether the induction
principle for the data type is derivable, but a result by Herman
Geuvers says that this is never the case, no matter which encoding is
used. However, if we add identity types to the (extensional) Calculus
of Constructions, this changes: by cutting down the Church encoding
to only the "natural transformations", we can construct strongly
initial algebras of arbitrary (even non-strictly positive) functors.

I'll give an introduction to impredicative encodings, and then
consider a baby version of the above result, and how it can be
extended to intensional type theories.

Friday 21st August 2015, 15:30
Board Room
Department of Computer Science