Structural Subtyping and the Notion of Power Type

Abstract

types We have used the term abstract type for types of the form P = Some(A:Type) B, because this models the concept of having an unknown type A which supports a set of operations of signature B. It should be pointed out that, unlike abstract types in second-order lambda calculus [Mitchell Plotkin 85] this notion of type abstraction does not prevent impersonation. That is, given a particular implementation p = pair(A:Type = C) b:B of P, the representation type C is visible, hence one can build an object of type A without using the operations in b. This problems can be partially solved by scoping techniques; e.g., a function which must operate on arbitrary implementations of P cannot make assumptions about any particular C. A complete solution to the impersonation problem requires introducing additional concepts [MacQueen 86]. On the positive side, the fact that even abstract types are matched by structure means that redefining an abstract type does not create a "new" one. This is co...