Hacker News Reader

Comment by seanmcdirmid | Hacker News Reader

Hindley-Milner is fun until you need nominal subtyping or mutable assignment, then the whole "semi-unification is undecidable in general" comes up to bite you.

View on HN

Weird points to make.

Subtyping isn't a good organizing principle for code reuse from a type-safety or human-sanity perspective. Typeclasses and composition are better.

You should give Haskell a whirl.

Haskell doesn't use Hindley-Milner.

Edit: Also, sub-typing tends to make a lot more sense in a language with value semantics, such as C++, than it does in a language like Haskell and isn't necessarily about organizing code.

What do you mean by value semantics here?

C++ gives you the freedom to choose between composition and subtyping to suit your problem without having to worry about an extra indirection if you choose composition.

For example, the base member of Composed is not a pointer as it might be in a language with reference semantics:

  struct Base
  {
      int i;
  };

  struct Derived : Base
  {
      bool b;
  };

  struct Composed
  {
      Base base;
      bool b;
  };

How does HM get in the way of mutable assignment?

Assignment is essentially similar to subtyping, if one says:

A := B

Then all values that could be bound to B could be bound to A also (so B <= A), but if the other way was also taken (B = A), then

A := C

Would imply that B = C, which leads to all sorts of safety problems...so you don't do that. At the end of the day, to make HM work with assignment, you need something like ML's "value restriction" that prevents full unification between A and B.

Nitpick: it's generalisation that is prevented by the value restriction. Unification works just fine:

    let test r =
      r := `A;
      r := `B;
      r := `C

r gets unified with all of `A, `B and `C: no problem.

Polymorphism (more precisely, generalization of unknown types) is incompatible with references. For example:

    let r = ref []

Here r has type 'a list ref (reference to a list of 'a where 'a is unknown).

    r := ["hello"]

r has type 'a list ref, := has type 'a ref -> 'a -> unit, and ["hello"] has type string list, so it works (if we instantiate 'a with string).

    let n = 1 + (List.head !r)

1 has type int, + has type int -> int -> int, and we can type (List.head !r) as int since we can type !r as int list since we can type r as int ref list (this time instantiating 'a by int).

So, we just added an int and a string and the program will probably crash. What's wrong is that every line is correct but because of the mutable store, the program as a whole is incorrectly typed.

The solution is to generalize only a subset of all syntactic constructs. The historic solution in Ocaml is to never generalize expressions that may allocate memory (that's the "value restriction") . For example, a function application (like f x, or ref []) may allocate, but a variable or a constant (like x or 1 or []) can not. That's why [] has type 'a list but ref [] has type '_a list ref ('_a can be unified only once, so in the above example an error would occur at the "let n").

Ahh, that's sort of obvious in retrospect, but I was blinded thinking in terms of Haskell where IO protects against such generalization.

The equivalent Haskell program is

    import Data.IORef

    main :: IO ()
    main = do
        r <- newIORef []
        writeIORef r ["Hello"]
        x <- readIORef r
        print $ x + 1
        return ()

The reference is bound by "r <-", ie a lambda (as this desugars to ">>= \ r ->"), and lambdas are never generalized (even in ocaml).

I think that the reason why it works is that because there is no way to let-bind r except with a toplevel unsafePerformIO.

Yup, that's precisely what I forgot to think about.

Yep, and also overloading, overall HM just isn't a good choice for a programming language.

Care to list the reasons why you believe HM just isn't a good choice for a programming language?

It limits the type system in order to achieve global type inference. HM is often touted as a "sweet spot" in static type systems because you don't have to specify types anywhere, but in reality it tends to be more verbose and less powerful than local type inference.

That hasn't been my experience, could you show me a small example?

In an HM system there is no overloading so you are essentially naming type constraints on every function call instead of once in the function definition.

C++ might look like this:

    void do_something(bar_t & bar)
    {
        ...
        bar.foo(...);
        bar.baz(...);
        auto something = bar.get_something();
        ...
    }

The equivalent Ocaml might look like this:

    let do_something bar =
        ...
        Bar.foo bar ...;
        Bar.baz bar ...;
        let something = Bar.get_something bar in
        ...

The situation is similar when dealing with structs and tends to be ever worse when dealing with generic code (although C++ only has duck typed generics until concepts comes along).

Reply on news.ycombinator.com