Type Definitions in Polya

Abstract

The programming language Polya maintains a clear separation between a type and its implementation through a new construct called the transform. Polya allows user to define their own data types and transforms to implement them. The type definition facility of Polya has capabilities not found in existing languages; in short, it allows a more comprehensive description of the properties that determine whether a program is well-formed. Two such properties are the scope of variables and the bounded polymorphic nature of some operations. One can specify the scope of any local variables that an operation introduces and express that the well-formedness of an operation depends on whether some overloaded function name stands for a function of a certain type. Also novel, is the ability to define literal classes for types and to specify both an abstract and concrete syntax for operations. With these capabilities, it becomes possible to define the syntax of a block-structured language within Polya itself.