Subtyping is Partial Evaluation

DeLesley Hutchins, University of Edinburgh

I am currently working on a calculus which combines types and objects into a single entity. Objects are treated as singleton types, and types are treated as ``abstract objects.'' In order to perform static type-checking, I introduce a subtype relation which is defined over both types and objects. Subtyping includes equivalence, and equivalence includes beta-reduction, so the type system blurs the distinction between typing and evaluation, and between run-time and compile-time. This unification brings together ideas from three different areas of computer science: dependent type theory, partial evaluation, and abstract interpretation.

I hope to generate a bit of discussion on these ideas, and hear comments and/or criticisms from the audience.