[Prev][Next][Index][Thread]
New technical report: Type Destructors
We are pleased to announce the availability of a new technical report
on "Type Destructors," available through:
http://www.cs.indiana.edu/hyplan/pierce/papers/td.ps.gz
This is an expanded version of the work that we presented at the FOOL
workshop a few weeks ago.
Enjoy,
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.