[Prev][Next][Index][Thread]
Multi-Level Specifications (new papers)
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
Multi-level specification is an extension of first-order many-sorted
algebraic specification that incorporates the definition of types in
the formalism itself. The following papers, available from
http://adam.fwi.uva.nl/~visser/types/mls/
, discuss the design and implementation of the modular, applicative,
multi-level equational specification formalism MLS. Comments are
welcome.
regards,
Eelco Visser
---
mail:visser@fwi.uva.nl
http://adam.fwi.uva.nl/~visser/
Multi-Level Specifications
--------------------------
Abstract. This chapter introduces a modular, applicative, multi-level
equational specification formalism that supports algebraic
specification with user-definable type constructors, polymorphic
functions and higher-order functions. Specifications consist of one or
more levels numbered 0 to n. Level 0 defines the object level
terms. Level 1 defines the types used in the signature of level 0. In
general, the terms used as types in level n are defined in level
n+1. This setup makes the algebra of types and the algebra of types of
types, etc., user-definable. The applicative term structure makes
functions first-class citizens and facilitates higher-order
functions. The use of variables in terms used as types provides
polymorphism (including higher-order polymorphism, i.e., abstraction
over type constructors). Functions and variables can be
overloaded. Specifications can be divided into modules. Modules can be
imported at several levels by means of a specification lifting
operation. Equations define the semantics of terms over a
signature. The formalism also allows equations over types, by means of
which many type systems can be described. The typechecker presented in
this chapter does not take into account type equations.
The specification, in ASF+SDF, of the syntax, type system and
semantics of the formalism is presented in three stages: (1) untyped
equational specifications (2) applicative one-level specifications (3)
modular multi-level specifications. The definition of a typechecker
for stages (2) and (3) is divided into four parts: (a) well-formedness
judgements verifying type correctness of fully annotated terms and
specifications, (b) non well-formedness rules giving descriptive error
messages for the cases not covered under (a), (c) a type assignment
function annotating the terms in a plain specification with types, and
(d) a typechecking function which checks well-formedness after
applying type assignment. These functions are defined uniformly for
all levels of a specification.
Aside of defining a new specification formalism, this chapter
illustrates the use of ASF+SDF for the design and prototyping of
sophisticated specification formalisms.
To appear in: A. van Deursen, J. Heering and P. Klint (editors)
Language Prototyping. An Algebraic Specification Approach. AMAST
Series in Computing, World Scientific Publishing Co., 1996.
A preprint is available as Technical Report P9604, Programming
Research Group, University of Amsterdam.
Solving Type Equations in Multi-Level Specifications
----------------------------------------------------
Abstract. In first-order algebraic specification functions have types
of the form s1 X ... X s_n -> s_0, where the s_i are type
constants. Such types exclude higher-order and polymorphic
functions. In multi-level algebraic specification the structure of
types used in function declarations is specified as an algebraic data
type. If only free constructors are used in the types used in function
declarations, type assignment is an extension of the Hindley/Milner
algorithm to multiple levels of types. By means of equations over
types, sophisticated type systems can be modeled in a simple and
uniform language. The type assignment for arbitrary multi-level
specifications requires E-unification. Although this is undecidable in
general, it is decidable for restricted sets of equations.
In an earlier paper, the modular applicative multi-level equational
specification formalism MLS is defined. The typechecker supports only
free type constructors.
In this paper we introduce multi-level specification by means of a
series of MLS examples and discuss the extension with an E-unification
procedure instead of syntactic unification of the type assignment
function for MLS such that it supports type definitions, defined type
operators and recursive types.