DDC/FurtherReading
< DDC
1 Introductions
- Type Inference and Optimisation for an Impure World Ben Lippmeier, PhD Thesis, Australian National University, Submitted June 2009.
- Witnessing Purity Constancy and Mutability Ben Lippmeier, Submitted to APLAS 2009.
2 On the development wiki
3 Related systems
The Disciple type system is a combination and extension of several existing systems.
For region typing:
Note that DDC uses regions to track mutability of objects, not to manage allocation.
- A Region Inference Algorithm, Mads Tofte and Lars Birkedal, ACM Transactions on Programming Languages and Systems, Vol 20, No 5, July 1998
For effect typing:
This is where DDC gets is namesake.
- The Type and Effect Discipline, Jean-Pierre Talpin and Pierre Jouvelot, Seventh Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, 1992
For closure typing:
Closure typing was originally intended for O'Caml, but was not fully implemented as it was thought to complicate the interface files too much. In Haskell and Disciple you don't have to write your own interface files, so this isn't a problem.
- Polymorphic type inference and assignment. Xavier Leroy and Pierre Weis, Proc 18th Symp. Principles of Programming Languages, 1991.
For the region/effect/closure class system:
The DDC core language uses witnesses to mutablity and constancy of regions, purity of effects and emptiness of closures. These witnesses are managed in much the same way as the type equality witnesses in System-Fc.
- System F with Type Equality Coercions, Martin Sulzmann, Manuel Chakravarty, Simon Peyton-Jones, International Conference on Functional Programming, 2006.
Talks about Disciple: