All modern approaches used for the definition of abstract types in programming languages do not allow values of these types to be used in pattern-matching. This limits the use of abstract types in programs. In this paper we propose a new form of abstract type definition, based on Wadler's notion of views, which allows pattern-matching for values of abstract types.
With our approach, a type definition provides, in a simple and uniform way, either a type synonym, a datatype, an abstract type, an abstract type with views, a subtype of an existing type, or a module (collection of declarations).
The paper presents a very simple semantics of a kernel language with the proposed type definition mechanism. The mechanism can be efficiently implemented, and can use pattern-matchin on constructors of the representation type whenever there is an isomorphism between (the relevant view of) the abstract type and its representation type; the decision of when such an isomorphism exists is simple and based directly on the abstract type definition.
With data type definitions, if a type (implementation) is changed then all program parts that perform pattern-matching on constructors of values of that type need to be modified. With
abstract type definitions, a representation may be changed without the need for these modifications, but no pattern-matching can be performed on values of this type. A type
with a view changes this situation. Its representation (implementation) may be changed without having to change user's code, if the view (interface) is not changed.