Algorithmic Type Inferencer Specifications For Declarative Type Systems
Stc
Date: 2009-04-09
Time: 11:45
Room: BBL room 471
Speaker: Arie Middelkoop
Title: Algorithmic Type Inferencer Specifications for Declarative Type Systems
Abstract
A
type system defines which types are valid for an expression. A
type inferencer tries to construct a most general valid type for an expression. Therefore, a type system serves as a specification for a type inferencer.
For non-trivial type systems, there is an enormous gap between specification and implementation. We are working on closing this gap by coming up with executable specifications. Type rules are not used as the language for our specification. Instead, we use
inferencer rules. These inferencer rules are similar to type rules, except that they contain annotations that describe how to actually perform computations.
When we straightforwardly transform the type rules into type inferencer rules, we encounter problems with declarative aspects of type rules. One particular problem is that a type rule may refer to a value that during inference is not available yet when the corresponding inference rule is executed. We solve this problem by providing annotations that deal with this problem in a specific way, but general enough to work for many type systems.
During this talk, I'll demonstrate this inferencer language and its semantics by means of an example: obtaining an inferencer from a relatively simple impredicative type system.
