We study a variant of System Fsub that integrates and generalizes
several existing proposals for calculi with STRUCTURAL TYPING RULES.
To the usual type constructors (->, #, All, Some, Rec) we add a number
of type DESTRUCTORS, each internalizing a useful fact about the
subtyping relation. For example, in Fsub with products every closed
subtype of a product S#T must itself be a product S'#T' with S'<:S and
T'<:T. We internalise this observation by introducing type
destructors .1 and .2 and postulating an equivalence T =eta T.1#T.2
whenever T <: U#V (including, for example, when T is a variable). In
other words, every subtype of a product type literally IS a
product type, modulo eta-conversion.
Adding type destructors provides a clean solution to the problem of
POLYMORPHIC UPDATE without introducing new term formers, new forms of
polymorphism, or quantification over type operators. We illustrate
this by giving elementary presentations of two well-known encodings of
objects, one based on recursive record types and the other based on
The formulation of type destructors poses some tricky meta-theoretic
problems. We discuss two different variants: an ``ideal'' system
where both constructors and destructors appear in general forms, and a
more modest system that imposes some restrictions in order to achieve
a tractable metatheory.