31.4 Notes
|
| < Free Open Study > |
|
31.4 Notes
Many of the ideas behind 
are due to Cardelli, particularly to his paper, "Structural Subtyping and the Notion of Power Type" (1988a); the extension of the subtype relation to type operators was developed by Cardelli (1990) and Mitchell (1990a). An early semantic model was given by Cardelli and Longo (1991) using partial equivalence relations. Compagnoni and Pierce (1996) gave a model for an extension of 
with intersection types. A more powerful model including recursive types was given by Bruce and Mitchell (1992); a related model can be found in Abadi and Cardelli (1996).
Basic metatheoretic properties of the variant of 
given here were proved by Pierce and Steffen (1994), and independently (using a cleverer proof technique that simplifies one of the main arguments) by Compagnoni (1994). Compagnoni's technique was also used by Abadi and Cardelli (1996) for a variant of 
with their object calculus, rather than the lambda-calculus, as its core term language.
The pointwise definition of subtyping between type operators can be generalized to allow subtyping between applications of different type operators to different arguments (F S <: G T) if we refine the kind system so that it tracks the polarity of type operators. We says that an operator F is covariant if F S <: F T whenever S <: T and contravariant if F T <: F S whenever S <: T. If we introduce two new subtyping rules reflecting these properties
then it follows (by transitivity) that F S <: G T if F <: G, S <: T, and G is covariant. To make all this work, we also need to mark type variables with their polarities, and to restrict higher-order quantifiers to range only over operators with certain polarities. Versions of 
with polarities have been considered by Cardelli (1990), Steffen (1998), and Duggan and Compagnoni (1999).
Another possible generalization of the presentation of 
used here is generalizing unbounded type operators λX::K1.T2 to bounded type operators λX<:T1.T2. This is an appealing step, because it matches the way we generalized quantifiers to bounded quantifiers when we formed F<: by adding subtyping to System F. On the other hand, it substantially complicates the system, since we must also generalize the kind system to include kinds like "X<:T1.K2; this, in turn, introduces a mutual dependency between the kinding and subtyping rules that requires significant work to untangle. See Compagnoni and Goguen (1997a; 1997b).
Extensions of 
with dependent types have been studied by Chen and Longo (1996) and Zwanenburg (1999).
|
| < Free Open Study > |
|
EAN: 2147483647
Pages: 262