Home » forums » LtU Forum

Learning Pragmatics of Implementing a "Modern" Type Systems

Subject line pretty much says it all - type systems as in ML, Haskell, Scala, etc.

I've tried comp.lang.compilers and comp.lang.functional to no avail. Help me Obi Wan, you're my only hope :-)

If this is not PLT enough a topic, I'll fully understand if the moderator deletes it.

Otherwise, many, many thanks in advance.

Scott

By scottmcl at 2008-12-28 19:45 | LtU Forum | previous forum topic | next forum topic | other blogs | 9714 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

The subject is ok, if I

The subject is ok, if I understand what it is you are asking about. I assume Pierce's book (TAPL) does not match your needs?

By Ehud Lamm at Sun, 2008-12-28 20:42 | login or register to post comments

Implementation approaches

Well, personally I'm increasingly finding that it makes sense to view type checking and type inference as (constraint) logic programming tasks. HM(X) Type Inference is CLP(X) Solving is about this, and one of Derek's favourite prolog demonstrations is that a typechecker for the simply-typed lambda calculus is also an inferrer. I've been playing with some related things too - if enough people nag me (Matt?), I'll take a hatchet to my IFL attempts and retrieve the parts that're both cool and reasonably solid!

By Philippa Cowderoy at Mon, 2008-12-29 01:40 | login or register to post comments

Nag

Nag nag nag! Get it done!

By Matt Hellige at Mon, 2008-12-29 20:31 | login or register to post comments

It'd be easier if you didn't ignore me!

Seeing as you're not responding to IRC messages I guess I'll have to link what I have: One odd Hindley-Milner variant with a funky implementation strategy. Further proddage will result in Haskell source for a checker that uses traditional unification as an implementation for the constraints, but the typing rules are syntax-directed and can be read straight off if you're happy keeping an explicit constraint set. That's not a bad idea if you're looking to handle error messages in the vein of Bastian Heeren's work.

I've toyed with qualified types in the same vein, and there's a pile of other things I'd like to try because I think there's a recipe of sorts that can be extracted from what I've done there. Right now though, I'm looking at using the elaboration technique to track back errors generated by a 'core' typechecker to sugared code - effectively having the desugaring pass provide a trail back to the source, but with a sensible approach to ensuring all the necessary info is present.

By Philippa Cowderoy at Tue, 2008-12-30 17:41 | login or register to post comments

Implementing Type Inference

I found the following resources helpful for understanding type inference, in order of increasing difficulty:

  1. Chapter 30 (Type Inference) of the freely available book PLAI, Programming Languages: Application and Interpretation, sketches unification-based type inference.
  2. The summer course Interpreting types as abstract values presents elegant evaluators, type checkers, type reconstructors and inferencers using Haskell as a metalanguage.
  3. Chapter 7 (Types) of the book EOPL, Essentials of Programming Languages.
  4. Chapter 22 (Type Reconstruction) of the book TAPL, Types and Programming Languages, and the corresponding OCaml implementations recon and fullrecon.
  5. Chapter 13 (Type Reconstruction) of the new book DCPL, Design Concepts in Programming Languages.
  6. Selection of academic papers.

However, since the best way to learn is to do, I strongly suggest implementing type inference for a toy functional language by working through a homework assignment of a programming languages course.

I recommend these two accessible homeworks in ML, which you can both complete in less than a day:

  1. PCF Interpreter (a solution) to warm up.
  2. PCF Type Inference (a solution) to implement algorithm W for Hindley-Milner type inference.

These assignments are from a more advanced course:

  1. Implementing MiniML

  2. Polymorphic, Existential, Recursive Types (PDF)

  3. Bi-Directional Typechecking (PDF)

  4. Subtyping and Objects (PDF)

By namin at Sun, 2008-12-28 22:43 | login or register to post comments

Hmmm....

First snow has fallen,
grey leaves may yet be unread,
seeking a flower.

.... Dude, where's the question?

By marco at Sun, 2008-12-28 22:52 | login or register to post comments

Clarification?

Are you looking for help implementing a/the type system or do you have a pretty good idea, and are looking for tips about implementing one well?

I mean, if you're looking to just implement one then pick an example (TAPL has one) and make it work and dabble if you're the sort that learns that way. Otherwise prototype one out, see what works; what doesn't... I'm maybe not a great example, but I found that *starting* with the type system worked best for me.

If you're looking for tips for making the implementation fast or otherwise better, a description of what you've got might help.

By RM Schellhas at Mon, 2008-12-29 03:47 | login or register to post comments

I'll try to clarify...

Well, I have some older books like Hollub's "Compiler Design in C", a nice but somewhat obscure book on writing compilers and interpreters based on Pascal implementation and so on (generally "Algol" and "Lisp" family languages). Depending on the volume, there's some theory (Hollub spends a little too much time on LL1 and LALR parsing, IIRC) and quite a bit of actual implementation code.

Now, what I'm particularly interested is a theory + practice treatment of a panoply of language type system features - type checking languages generics, constrained generics, local type inference, type level treatment of modern object oriented languages (single/multiple inheritance, multi-methods, co/contra variance, etc.), a nice treatment of HM, type inference for recursive functions, and so on and so so forth.

I'm certainly open to other suggested topics from which I will profit by addressing.

I understand that one volume might not cover all of these topics well, so I'm open to multiple suggestions.

Again, many thanks.

Scott

By scottmcl at Mon, 2008-12-29 06:56 | login or register to post comments

Go get yourself a copy of

Benjamin Pierce's tome, Types and Programming Languages, available from an online bookseller near you. This book, frequently referred to 'round here as TAPL, is the definitive work on type theory.

A second book is Advanced Topics in Types and Programming Languages. This is also recommended; but isn't really a traditional textbook; instead it's an edited collection of papers reflecting some of the current research in the field. Pierce is the editor here, but FTMP not the author.

A third book, if you are interested in OO type theory, is Adabi and Cardelli's work A Theory of Objects; which puts much of OO programming on a rigorous formal footing.

One other interesting book to consider are Chris Date's Types and the Relational Model; albeit Date is more knowledgeable about databases than he is about type theory, and his presentation style and nomenclature is a bit strange to those coming from a FP background.

(Sorry about the broken tags in the original post; I went to edit them and found that someone had done so already)

By Scott Johnson at Tue, 2008-12-30 00:41 | login or register to post comments

Use your head

That's the best advice I can give you. Judging from the ml-sources of TAPL it will give a very instructive introduction into terminology, logics, and current algorithms. That, might, probably will, be sufficient as an introduction to the current field.

However, (I am somewhat of a fan) Dijkstra was notorious for never reading any articles in the field since it clouded his judgements. If you start of with plain HM, I think if you analyze most of the algorithms roughly, you might actually come up with most of them yourself.

I personally understand most algorithms as simplified tactics on sequent calculi, so that is how I implement type systems [as constraint solvers]. A proof of equality is a unification tactic, generalization and specialization are rules on existential and universal quantifier introduction and elimination, equality of recursive types can be proven by co-inductive arguments, etc. You might want to read up on that too.

By marco at Wed, 2008-12-31 00:23 | login or register to post comments

I personally understand most

I personally understand most algorithms as simplified tactics on sequent calculi

I'd second this intuition. What I was doing with PrenexF (linked above) was essentially trying to make the appropriate tactics blindingly obvious!

By Philippa Cowderoy at Wed, 2008-12-31 00:31 | login or register to post comments

Re: type systems as sequent calculi solvers

things like Qi make that approach explicit, if i understand correctly.

By raould at Fri, 2009-01-02 22:51 | login or register to post comments