Abstract
Type and effect systems are typically specified as a system of
logical deduction rules, which specify what are valid types and
effects in a program. Converting such a system into an algorithm
is typically a lot of error-prone work, and usually results in an
implementation that performs its task inflexibly, leaving no room
to modify the solving strategy, without changing the algorithm.
In this paper we take a constraint-based approach to declaratively specify a type system. Our contribution is to enrich the type
rules by the use of a fixed set of combinators. By choosing a semantics for these combinators, we obtain particular orderings of
the constraints, which can then be fed into a constraint solver. Thus they bridge the gap between the declarative specification and a deterministic implementation of type systems. The main advantages are that the issue of the order in which constraints should be solved is factored out of the solver, making the solver simpler and more amenable to reuse; the user of the solver can flexibly choose a particular solving strategy; and it makes the implementation of type and effect systems a much easier and less error-prone task. Our combinators have been implemented into a fully functional compiler.
logical deduction rules, which specify what are valid types and
effects in a program. Converting such a system into an algorithm
is typically a lot of error-prone work, and usually results in an
implementation that performs its task inflexibly, leaving no room
to modify the solving strategy, without changing the algorithm.
In this paper we take a constraint-based approach to declaratively specify a type system. Our contribution is to enrich the type
rules by the use of a fixed set of combinators. By choosing a semantics for these combinators, we obtain particular orderings of
the constraints, which can then be fed into a constraint solver. Thus they bridge the gap between the declarative specification and a deterministic implementation of type systems. The main advantages are that the issue of the order in which constraints should be solved is factored out of the solver, making the solver simpler and more amenable to reuse; the user of the solver can flexibly choose a particular solving strategy; and it makes the implementation of type and effect systems a much easier and less error-prone task. Our combinators have been implemented into a fully functional compiler.
Original language | English |
---|---|
Publisher | Department of Information and Computing Sciences, Utrecht University |
Number of pages | 10 |
Publication status | Published - 2006 |
Publication series
Name | Technical Report Series |
---|---|
No. | UU-CS-2006-055 |
ISSN (Print) | 0924-3275 |