Hacker News new | comments | show | ask | jobs | submit login

But you don't need to understand any of the H-M algorithm to understand how to use a language with a H-M type system. You just need to understand that every expression in your program must be able to be statically assigned a non-union non-dependent type.

If an expression can't be assigned such a type (e.g. it's sometimes an integer and sometimes a string (in the same function call); or it's a non-empty list, etc.) then your program won't type. Otherwise it will.

Importantly: it doesn't matter how you come to this conclusion; the compiler will use the H-M algorithm, but that doesn't mean you need to. You can just look at your "if" expression and realize that you're returning an integer in one branch and a string in the other and that that violates the "non-union non-dependent" requirement above.

(This, BTW, is an example of the difference between a spec (what I outlined above) and an implementation (what the H-M algorithm says to do).)

This is an excellent point, and we're in vehement agreement. Or almost vehement agreement.

The thing is, as a programmer, I have to understand what result the algorithm will produce. I have to understand what type my variable will be. If I have to look and see what the compiler came up with, I have way too much work to do.

There are two ways to solve this problem. One is to build an abstract mathematical model which you can emulate in your head - not using the same methods, maybe, but getting the same results. The other is to build a concrete, mechanical model which you don't emulate, but rather simulate. Your brain computes not the goal of the algorithm, but the mechanism by which the algorithm is implemented. Same result - you know what type the variable will be.

From my perspective, it's one problem, it has to get solved, and the right way to solve it is the way that's the easiest for the people who will actually use the language. For my kind of people, I feel math guys are far too enamored of doing it the emulation way instead of the simulation way.

But this is basically an aesthetic opinion about user interface design, so we may be at the end of Hume's is-ought question here...

As a side note, you should check out Erlang's static checker, Dialyzer. It implements a complete (i.e. no-false-positives) type system, as opposed to a sound (i.e. no-false-negatives) type system (e.g. H-M and friends). It pretty much eliminates the need to make any predictions about what the type checker will say, as it will only complain if your program can provably crash due to a type error.

Of course this still permits the possibility of type errors, but in practice it works fairly well, and does not constrain the programmer.

Dialyzer is decent, given the constraints for which it was designed, but nowhere near as helpful as a ML-derived static type system.

For example, Dialyzer won't reject a function declared to return values of type A and actually returning values of type B along an execution path which isn't currently traveled.

In practice, using a language with Hindley-Milner type inference is massively more simple than you appear to think it is. There are countless other warts, but this ain't it.

I sense a fallacy lurking here. Sure, a type system like Haskell's or even Scala's is magic (and can be used without understanding it) as long as it can "Do What You Mean," but when it can't, you have to understand its workings. We can't sweep that fact under the rug by calling any failure to "Do What You Mean" a bug, a wart to be fixed -- a deviation from correct DWYM behavior. There is no actual DWYM type system, or at least no one's ever come up with one.

What type system doesn't have warts? Haskell's probably has both more and fewer than most, depending on how you count them, because so much emphasis is put on the type system.

When you use any language long enough, you end up needing to simulate pretty much every observable aspect of it yourself -- not including, for example, the garbage collector, the JVM bytecode verifier, or the GCC code optimizer, which are supposed to be transparent, but including the type inferencer, the JVM threading model, and the JavaScript semicolon insertion rules, which are not. Some of these things you can steer clear of for a long time or even avoid forever by staying on the beaten path, but they lurk, waiting for the thousands of people who have run into bugs or compiler errors and needed to understand them.

I don't know HM too well, but it seems to have more in common with the dataflow analysis algorithms in optimizers and verifiers -- which programmers don't usually have to understand -- than the basic unidirectional type inference that already serves pretty well to reduce redundancy in the source code.

Let's not confuse Hindley-Milner type inference with Haskell's (or ML's) type system.

While Haskell's type system can be complex, depending on the exact language extensions in play, Hindley-Milner type inference is simple. It's just good UI — you almost never need to write explicit type declarations, because the compiler (or typechecker) can almost always figure out what you mean. That's it!

Using advanced Haskell extensions can occasionally require annotating a non-top-level value with a type, in order to resolve an ambiguity. The compiler will point out which value has an ambiguous type.

Also, if you've made a mistake and your program doesn't typecheck, depending on whether explicit type declarations have been provided or not, the compiler may complain about different parts of the program. Adding type annotations may help pinpoint the exact location of the mistake. This isn't really a problem, and it's more of an issue in SML and OCaml than Haskell, because these languages don't encourage annotating top-level values with types.

There is never any need to simulate any part of the Hindley-Milner type inference algorithm in your head. The algorithm's only failure mode is a request for more information, and the requested information should already be obvious to you, the programmer, as programming in a ML-derived language means thinking in terms of typed values.

The warts I had in mind were problems with the Haskell ecosystem, such as Cabal hell, or the Haskell community, such as a tendency towards academese — not anything to do with its type system, or type inference mechanism.

In a stark contrast, Scala's "type inference" is not Hindley-Milner, and is barely able to infer the existence of its own arse with both hands, failing in even the simplest of cases.

Example 1. Unable to infer type of `optBar`, because `None` is also a type:

    scala> class Foo {
         |   def setBar(bar: Int) = optBar = Some(bar)
         |   def getBar = optBar.get
         |   var optBar = None
         | }
    <console>:8: error: type mismatch;
     found   : Some[Int]
     required: object None
             def setBar(bar: Int) = optBar = Some(bar)

    scala> class Foo {
         |   def setBar(bar: Int) = optBar = Some(bar)
         |   def getBar = optBar.get
         |   var optBar: Option[Int] = None
         | }
    defined class Foo
Example 2. Unable to infer type of `foobar`, with uncurried `foo`:

    scala> def foo(bar: Int, baz: Int) = bar + baz
    foo: (bar: Int, baz: Int)Int

    scala> val foobar = foo(1, _)
    <console>:8: error: missing parameter type for expanded function ((x$1) => foo(1, x$1))
           val foobar = foo(1, _)

    scala> val foobar = foo(1, _: Int)
    foobar: (Int) => Int = <function1>
Workaround, with curried `foo`:

    scala> def foo(bar: Int)(baz: Int) = bar + baz
    foo: (bar: Int)(baz: Int)Int

    scala> val foobar = foo(1)_
    foobar: (Int) => Int = <function1>
Which languages have "basic unidirectional type inference"? I'm not familiar with the term.

Scala […] is barely able to infer the existence of its own arse with both hands, failing in even the simplest of cases.

Thanks for this. Not only did I lol, but this confirmed my suspicion that Scala was "not the language I was looking for" to use for an upcoming project (a compiler that, for business/politics reasons, must run on the JVM). You've no doubt spared future me regret.

Check out ermine[1], a language for the JVM that was written for exactly that reason. It's being used at S&P Capital IQ. You can look at the user guide[2] for more information.

[1]: https://github.com/ermine-language

[2]: https://launchpad.net/ermine-user-guide

Thanks for pointing it out!

> One is to build an abstract mathematical model which you can emulate in your head

The ability to emulate your abstract or concrete programming model in your head cannot be overemphasized. I used to program the original 8-bit B&W Gameboy, which was a machine so simple and small I could literally emulate it at the clock cycle level while I was writing the code for it.

If you can fit your model into your cache (brain) you can do amazing things using just your wetware.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact