## 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 |