Polymorphic regular tree types and patterns

We propose a type system based on regular tree grammars, where algebraic datatypes are interpreted in a structural way. Thus, the same constructors can be reused for different types and a flexible subtyping relation can be defined between types, corresponding to the inclusion of their semantics. For instance, one can define a type for lists and a subtype of this type corresponding to lists of even length. Patterns are simply types annotated with binders. This provides a generalization of algebraic patterns with the ability of matching arbitrarily deep in a value. Our main contribution, compared to languages such as XDuce and CDuce, is that we are able to deal with both polymorphism and function types. Categories and Subject Descriptors D.3.3 [Programming Languages]: Language Constructs and Features ? Patterns, Polymorphism, and Data Types and Structures; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs ? Type Structure General Terms Algorithms, Design, Languages,...

• Type: Conference
• Year: 2006
• Where: POPL
• Authors: Jerome Vouillon
• Keywords: Flexible Subtyping Relation, POPL 2006, Programming Languages, Regular Tree Grammars, Structure General Terms