|
Mini Component Pascal was completed as the major work product of an honours project
by Brian Blackwell. The immediate predecessor of this project was another honours
project by Simeon Cran. As part of his honours thesis, Cran ported a type inferencer
by Luca Cardelli for a small functional language that supports ML-style polymorphism.
This type inferencer formed the basis of the Mini Component Pascal compiler implementations.
An online version of this type inferencer is available.
From Cran's honours thesis:
This part of the project was based around
a paper by Luca Cardelli
that is designed to illustrate the Hindley-Milner type inferencing algorithm. The paper
discusses the algorithm in detail, and includes a partial implementation written in Modula-2.
Cardelli has omitted modules from the code that are required to actually test and observe the
implementation: most significantly, there is no scanner, parser, driver, or error handler. It
was decided to port the Cardelli code to Component Pascal, and to create the missing modules
so that a type inferencing program could be built and observed [...]
Cardelli presentation of the algorithm uses a typed version of the Lambda calculus, noting
its similarity to a simplified version of Milner’s language ML. The type inferencing program [...]
parses and types programs of this simple language, and further examples are based on it.
The concrete syntax of the language supported by the type inferencer is as follows:
Exp ::=
Ide |
"if" Exp "then" Exp "else" Exp |
"fun" "(" Ide ")" Exp |
Exp "(" Exp ")" |
"let" Decl "in" Exp |
"(" Exp ")"
Decl ::=
Ide "=" Exp |
Decl "then" Decl |
"rec" Decl |
"(" Decl ")"
The type inferencer comes with a number of functions pre-loaded into the environment:
| Operator | Type |
| true, false | bool |
| 0 | int |
| succ, pred | int -> int |
| times | int -> (int -> int) |
| plus | int -> (int -> int) |
| minus | int -> (int -> int) |
| eq | int -> (int -> bool) |
| zero | int -> bool |
| pair | A -> (B -> (A x B)) |
| fst | (A x B) -> A |
| snd | (A x B) -> B |
| nil | [A] |
| cons | (A x ( [A])-> ( [A]) |
| hd | [A] -> A |
| tl | [A] -> A [A] |
| null | [A] -> bool |
| inl | A -> (A + B) |
| inr | B -> (A + B) |
| outl | (A + B) -> A |
| outr | (A + B) -> B |
| isl | (A + B) -> bool |
| isr | (A + B) -> bool |
|
