Type And Effect Systems
Apa
Welcome to the Type and Effect Systems project.
As for the previous project on Dataflow Analysis and Abstract Interpretation,
there is some flexibility in the project, most notably in your choice of analysis.
However, this time there are some constraints:
- the language must be higher-order (i.e., based on the lambda-calculus), and include a variety of constructs such a numerals, application (duh), conditionals, local definitions in order to write interesting example programs
- you must use a type and effect system approach
- there must be an implementation of the type system
- a sizable number of the following to concepts should play a role in your assignment: unification, Algorithm W, polyvariance, subeffecting/subtyping.
- follow the two-stage approach: unify and generate constraints during the first, solve constraints in the second.
The following aspects are always negotiable:
- which extensions to the lambda-calculus will be supported (recursion, data structures, assignments, communication, exceptions)
- which analysis to perform (below you can find some suggestions)
- in which language to make the implementation (Haskell is advised)
- if you choose a concrete language to analyse (OCaML? , Clean, Haskell), what parts of the chosen language will be omitted (and possible other restrictions).
- lazy or strict
Use the following two projects as a source of inspiration for project (or simply choose and do one of these).
Do check back with me if you want to a variant.
Control-flow analysis with data-structures
Consider a lambda-calculus with facilities for data structures (lists, pairs, general datatypes).
You may add syntax to define (and not only use) data types, but this is not essential.
Add a case-statement to the language.
Perform a control-flow analysis of this language, so that you can track, in addition to the
creation points of functions, also the creation points of data structures.
This is Mini Project 5.2 from Nielson, Nielson and Hankin, so look there for some more information.
Polyvariant strictness analysis with seq
This project is based on some papers of ours: take the strictness analysis of our PEPM 2010
paper, first make it polyvariant, and for the not so faint of heart, consider minimal typing
derivations for this polyvariant analysis (as in our paper at LDTA 2010).
Links to the papers can be found under
CourseLiterature.
Generic Type and Effect Systems
Read the paper by Millstein and Marino
To ACM Portal
After doing so, come over and discuss with me what you might implement based on the ideas in this paper.
Note that this has nothing to do with Generic Programming!
Polyvariant Control-Flow Analysis for a Polymorphic Lambda-Calculus
Then maybe consider minimal typing derivations for this system.
Units of Measure
This is Mini Project 5.5 from Nielson, Nielson and Hankin. Consider it for more details. You can borrow the book if need be.
Communication Analysis
Consider Section 5.5 from Nielson, Nielson and Hankin on Communication Analysis.
Devise an implementation for this analysis and experiment with it. According to the book itself, this is complicated.
Oh yes...
For formulating the type system in LaTeX. I have made some Lhs2Tex code written by Stefan available
here.
You can sue these files as a basis for your documentation, as we do for our papers.
In all cases, I expect a working implementation, good examples, a type system specification and an explanation
of both the type system, a run through of one or two examples and an architectural description of the implementation.
Features and limitations should be prominently displayed in your documentation.
You may use any lexer, parser and type inferencer that you have already developed for the course Compiler Construction.
--
JurriaanHage - 17 Jun 2010
