DDC/FurtherReading

The Disciple type system is a combination of several existing systems that have been around for some time. Until the DDC dev-teams's thesis is finished (erk), these papers would be a good start if you wanted more information about how it works.

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 constness 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, which is where I got the idea from.

• System F with Type Equality Coercions, Martin Sulzmann, Manuel Chakravarty, Simon Peyton-Jones, International Conference on Functional Programming, 2006.