Hindley-milner type system

[Drup]

This add the language "hm", which is a direct implementation of an hindley milner type system for an impure ml-like language. This supports references, first class function, fixpoint and type inference of polymorphic types with value restriction. The type inference algorithm is the one presented in Oleg's article.

I was slightly unsatisfied with the fact that the language called ml didn't actually had an ML type system, so I added it. :)

One small annoying fact of this implementation is that the operators are all prefix, instead of infix, for the simple reason that I didn't bother writing the grammar for infix operators. In order to make the internal behavior of the typechecker more apparent, all internal ids are shown using fancy utf8 subscripts:

% ./hm.native
HM -- programming languages zoo
Type Ctrl-D to exit
HM> let id = fun x -> x ;;
id₃ : '₄ -> '₄ = fun x₂ -> x₂
HM> let notid = id id ;;
notid₅ : ('_₇ -> '_₇) = fun x₂ -> x₂
HM> let b = notid 3 ;;
b₉ : int₀ = 3
HM> let _ = notid ;;
_₁₁ : int₀ -> int₀ = fun x₂ -> x₂

[andrejbauer]

Thanks.

1. There are some stylistic changes that should be made before we can pull this (such as not opening the Syntax module everywhere).
2. There are too few comments for the code to count as "educational".
3. And I'd prefer an evaluation strategy that doesn't perform direct substitution.

Did you notice that we have poly already, which does parametric polymorphism (but not let-polymorphism and no value restriction)? Maybe we could base this language off that one, so that people can first look at poly and then at this language as an extension of poly. That way they can notice the difference between parametric polymorphism and Hidnley-Milner.

[Drup]

I noticed you have poly yes, but I'm not sure what you mean by "an extension". The language is quite different (much bigger surface in poly, but the typechecking algorithm is very different and simpler). The goal here is really to demonstrate generalization/value restriction. The typechecking algorithm has pretty much nothing in common.

I feel like making the surface language bigger would only result in more boilerplate and be less self-contained, which is pretty contrary to having something educational.

On substitutions ... would you prefer a big step with environments? I'm not sure it would make things simpler or clearer (the interpreter is not the interesting part anyway).

I can try to add more comments when I have some free time.

[andrejbauer]

I think I know how to do this. I'd like to keep the languages nice and clean, but at the same time I don't want to reject other people's contributions just because I think their code needs to be stylistically slightly different. How about if we introdue a contrib section of the source where we accept new languages liberally. Once they get cleaned up (commented properly, conform to stylistic guidelines) they can be moved to src. Would that work?

[Drup]

Sure, I don't mind at all. Although I wouldn't mind knowing what coding style you want. :)

[andrejbauer]

The guidelines are here. You are using open Syntax all over the place (point 9). You do not have interface files (point 7).

The non-stylistc comment is that I would prefer an evaluation loop which carrier an environment and computes from expressions to a datatype of values, rather than one that performs explicit substitutions. This will also simplify your printing functions, as you will only have to print values (and you don't print bodies of function closures). We can do this improvement later.

If you do these, I'll accept the language:

1. remove the open Syntax (except possibly in the parser)
2. create some interface .mli files for the modules
3. put in a bit more comments as to what is going on, these should be comparable to the amount of comments in the other languages.

Does that sounds reasonable to you?

[Drup]

Sure, that sounds perfectly reasonable. I'm not sure when I'll have time to play with this again, but I'll ping you when it's done. :)