New technical report: Type Destructors

We are pleased to announce the availability of a new technical report
on "Type Destructors," available through:


This is an expanded version of the work that we presented at the FOOL
workshop a few weeks ago.


        Martin Hofmann
        Benjamin Pierce


                          TYPE DESTRUCTORS

            Martin Hofmann               Benjamin C. Pierce
     Technische Hochschule Darmstadt     Indiana University

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
existential packages.

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, F^TD, which imposes some restrictions in order to
achieve a tractable metatheory.