It might be worth learning an ML-family language | Hacker News Reader

It might be worth learning an ML-family language

drmaciver.com

53 pointsjodooshi34 comments

You get much more than type-checking from ML-style languages.

It's worth learning one of these languages well enough to understand the fundamental concepts at play. If all you can see is static type analysis and arcane signatures you haven't dug deep enough yet.

The renaissance of functional programming happening in JS is the only thing that makes me happy about working in that language. Having immutable.js, ramda, ramda-lens, redux, and various monads (such as data.task and data.maybe) makes my code much more effective than using the majority of JS's more dynamic features... and it doesn't even have static type analysis.

My alma mater's introductory CS course was entirely in Standard ML, and was a great (if occasionally painful) way to learn some of the fundamentals of CS without requiring any background knowledge.

Julia is interesting in this regard (and Go I think - I used it's ancestor: Limbo). You can start with

    function foo(bar)
        pass
    end function

and then add types later when you've found out what was inferred

    function foo(bar::Int64)
        pass
    end function

I enjoy this style, it means I can create the story as I go along without re-writing types every time

Wait, does Julia really use the syntax `end function` to end a function? I haven't seen that kind of redundancy since I first learned how to program inside QBasic 3 for MS-DOS!

It doesn't, not sure where GP got that from.

no, I forgot, so many languages :)

I think I remembered that from endfunction in Octave

The benefit of inference is that you get the best of both worlds: you don't manually type-annotate anything, yet types are still statically checked. Does Julia do this?

Common Lisp does this too:

    (defun foo (bar))

vice

    (defun foo (bar)
      (declare (fixnum bar)
               (ignorable bar)))

And of course then the compiler can gripe if you try to call (foo "123").

> people routinely seem to get confused as to whether something is a value of a type, a strategy for producing values of that type, or a function that returns a strategy for producing the type.

In other words, they aren't sharp enough thinkers. It's the same problem as conflating singleton lists or sets with their lone element, constant functions with their output value, or “any list” with “list of anything”. Dijkstra put it quite nicely:

> About the use of language: it is impossible to sharpen a pencil with a blunt axe. It is equally vain to try to do it with ten blunt axes instead.

News just in: Languages with static type systems give better errors about types.

I think you missed the point. The author didn't say learn Java, Go, or C, for example.

"I think the reason for this is that in an ML family language, where the types are static but inferred, you are constantly playing a learning game with the compiler as your teacher'

This is not only missing the point, it's easy to prove false:

Python: `foo = '1' + 1` gives `TypeError: Can't convert 'int' object to str implicitly`

C: `char bar[] = "1"; char* foo = bar + 1;` gives literally no error.

Good errors occur because of strong/weak typing, not because of static/dynamic typing.

You always need to check array bounds in C, what else is new?

Apparently it's new to some people that C is a statically-typed, weakly-typed language.

If you're talking about the cast from an int literal to a char pointer, that's not what's happening. That's common C shorthand for incrementing a pointer to point to the next element.

For example, the char pointer increment compiles to:

  4004fb:	48 83 c0 01          	add    $0x1,%rax

While an int pointer increment compiles to:

  40050c:	48 83 c0 04          	add    $0x4,%rax

Because on my particular platform, an int is 4 bytes and a char is 1 byte and the memory is byte addressable.

I'm aware of what's happening. It's definitely a norm in C and it produces desirable results in many cases (I've written similar structures myself many times). All I'm saying is that from a type perspective it's a bizarre choice to allow that.

Good errors messages occur because you have enough information to craft said messages. Python has its fair share of utterly uninformative error messages, mostly due to the language's inability to comprehend the structure of user-defined types. Python programmers don't call these “type errors”, but a Haskell or ML programmer would.

Okay, but how do you gather enough information to craft said messages? I posit that there's nothing stopping you from gathering that information at runtime; it just typically isn't done to the same extent in dynamic languages as in ML-family languages.

A type system that gathers lots of type information is equivalent to a strongly-typed language IMHO, and a type system that gathers little type information is a weakly-typed language. Static languages can be strongly typed (Haskell, ML) or weakly typed (C) and dynamic languages can be strong(ish)ly typed (Python) or weakly typed (JavaScript).

> Okay, but how do you gather enough information to craft said messages?

There are two sources of such information: the static context (e.g., in Scheme, which variables are in scope) and the dynamic environment (e.g., again in Scheme, the type of an object, and, in Python, pretty much everything). The static context grows whenever you bind variables in the program text (e.g., when you define a procedure). The dynamic environment grows when the control flow reaches such binders (e.g., when it enters a called procedure).

> I posit that there's nothing stopping you from gathering that information at runtime; it just typically isn't done to the same extent in dynamic languages as in ML-family languages.

A fundamental limitation of dynamic analysis (that applies to any dynamic language, already invented or to be invented in the future) is its inability to “peek into the future”. For example, if you create an empty mutable list object, dynamic analysis can't tell you what its element type is supposed to be, until you actually start inserting elements into it. Static analysis, on the other hand, can determine what the element type is solely from inspection of the program text, e.g., if you make a procedure that inserts strings into the list, the list's element type must be a supertype of string, whether you actually call the procedure or not.

Here's an example of a type error that Python couldn't possibly diagnose: http://ideone.com/0KUVVb

> A type system that gathers lots of type information is equivalent to a strongly-typed language IMHO

This isn't true. C++'s type system gathers a lot of type information, yet C++ isn't “strongly typed” (assuming that term means anything at all) by any stretch of the term.

Rather than “strongly-typed”, a more useful term is “sound”. A type system is sound when it actually protects the language's basic abstractions. For example, Standard ML has a sound type system, and there's a formal proof of this fact. Java's type system is actually unsound, but it makes up for this deficiency by inserting runtime checks to turn wrong operations (e.g., invalid downcasts) into runtime exceptions (just like in Python!). C++'s type system is also unsound, and performing wrong operations is simply undefined behavior.

> There are two sources of such information: the static context (e.g., in Scheme, which variables are in scope) and the dynamic environment (e.g., again in Scheme, the type of an object, and, in Python, pretty much everything). The static context grows whenever you bind variables in the program text (e.g., when you define a procedure). The dynamic environment grows when the control flow reaches such binders (e.g., when it enters a called procedure).

Heh, I intended that as a rhetorical question, but I admit that wasn't clear from my post, and this is a very thorough answer. :)

> For example, if you create an empty mutable list object, dynamic analysis can't tell you what its element type is supposed to be, until you actually start inserting elements into it.

That's a limitation of most implementations of mutable list objects in dynamically typed languages, but there's nothing preventing a dynamic language from having a mutable list that enforces a single type in a list at runtime starting from the construction of the list. In Python it would not be difficult to implement an `IntegerList` class which enforces that all its elements are integers, for example.

Yes, we can't determine at compile time that the following is a type error:

    a = IntegerList()
    a.append('Hello, world')

But we can report on that at runtime (remember, I'm talking about the quality of type errors, not when they occur).

Further, one can imagine a hypothetical dynamic language where we parameterize types, too:

    a = List<Integer>()
    a.append('Hello, world')

Of course this could be implemented statically, but it could be implemented dynamically, the difference being that the type error would be reported at runtime instead of compile time. The reason, I think, that this isn't done is that once you get to the point where you're putting type parameters like this, you've lost most of the benefits of a dynamic type system, and would gain more from seeing your errors at compile time.

> > A type system that gathers lots of type information is equivalent to a strongly-typed language IMHO

> This isn't true. C++'s type system gathers a lot of type information, yet C++ isn't “strongly typed” (assuming that term means anything at all) by any stretch of the term.

You're right, I can't imagine what brain fart caused me to say what I said there. /shrug

> Rather than “strongly-typed”, a more useful term is “sound”. A type system is sound when it actually protects the language's basic abstractions. For example, Standard ML has a sound type system, and there's a formal proof of this fact. Java's type system is actually unsound, but it makes up for this deficiency by inserting runtime checks to turn wrong operations (e.g., invalid downcasts) into runtime exceptions (just like in Python!). C++'s type system is also unsound, and performing wrong operations is simply undefined behavior.

"Soundness" is a mathematically defined concept, but a very binary one (it's sound or it isn't). "Strength" is a different concept which admittedly isn't an objective measure. But I think we can agree on it as a subjective measure for comparing some things. For example, I do think there's a real phenomenon described that we can agree on when I say that Python is more strongly-typed than JavaScript, and Java is more strongly-typed than C, and I think you'd agree with me on these comparisons, even though none of these languages are soundly typed. Sound typing corresponds to a very strong type system. :)

> Yes, we can't determine at compile time that the following is a type error: (snippet)

> Further, one can imagine a hypothetical dynamic language where we parameterize types, too: (snippet)

If you're going to take the trouble to specify that it's an integer list, might as well use a statically typed language, right? When you use a dynamically typed language, presumably the point is to not have to worry about static types.

> The reason, I think, that this isn't done is that once you get to the point where you're putting type parameters like this, you've lost most of the benefits of a dynamic type system, and would gain more from seeing your errors at compile time.

Yep, exactly. The optimal tradeoff is that you don't anotate anything, yet static types are still there. What you described achieves the exact opposite.

> "Soundness" is a mathematically defined concept, but a very binary one (it's sound or it isn't).

That's precisely why it's better!

> For example, I do think there's a real phenomenon described that we can agree on when I say that Python is more strongly-typed than JavaScript,

Out of the box, Python certainly catches more errors than JavaScript, and does so earlier.

> and Java is more strongly-typed than C

I'm not so sure about this one. Although Java is certainly safer than C, because it replaces undefined behavior with a battery of runtime checks (just like a dynamic language), I feel it's about equally difficult in Java and C to translate my thoughts into types. Ironically, C++, despite being unsafe and unfixably so, does a much better job of helping me arrange things so that my errors are caught statically.

> If you're going to take the trouble to specify that it's an integer list, might as well use a statically typed language, right? When you use a dynamically typed language, presumably the point is to not have to worry about static types.

Yes, I said that. :)

> > "Soundness" is a mathematically defined concept, but a very binary one (it's sound or it isn't).

> That's precisely why it's better!

Well... it's better for some purposes, but it doesn't allow us to talk about most languages effectively. None of the top 10 most commonly-used languages in industry today are soundly typed. If memory serves me, in fact, the only language I know of with a mature implementation that's soundly typed is ML. So it's a useful concept in a very specific context, but not that useful for talking about most languages.

> I'm not so sure about this one. Although Java is certainly safer than C, because it replaces undefined behavior with a battery of runtime checks (just like a dynamic language), I feel it's about equally difficult in Java and C to translate my thoughts into types.

Basically I think what you're describing about Java is a mixture of mid-strength static typing and relatively strong dynamic typing. At least, that's how I'd describe it.

C does no real checking i.e. around `void` pointers, adding integers to pointers, tagging unions, etc., at compile time or at runtime, which is why I claim it's a very weakly-typed language (and also why I tend to avoid some of those features).

> Basically I think what you're describing about Java is a mixture of mid-strength static typing and relatively strong dynamic typing. At least, that's how I'd describe it.

For me, the real payoff of using a static type system is enforcing the invariants I care about. In other words, a type system is a tool that partially relieves me of my proof obligation as a programmer. A “type system” that doesn't do this is just annoying ceremony. So, if we insist on calling type systems “strong” and “weak”, this is still a binary question: a type system is either capable (“strong”) or incapable (“weak”) of expressing what I want to express in a crisp, elegant, crystal clear way. From this point of view, Java is just as unacceptable as C, perhaps even more so, because C at least has the decency not to pretend it has much of a type system.

OTOH, it seems that, to you, and perhaps most programmers, a type system is merely a tool for preventing catastrophic errors. If that's your only goal, then turning catastrophic errors (say, memory corruption) into less catastrophic ones (say, raising exceptions everywhere) is a perfectly valid approach, and of course Java is “more strongly typed” than C. This can be useful or harmful, depending on what kind of program you're writing, but I refuse to call it a type system.

Static+strong typing is a nice combination, which is probably what hacker_9 meant to say.

ML family is particularly nice -- with Hindley-Milner type inference, you get a lot of static guarantees with none of the verbosity of languages like Java.

It's not just type inference that makes programming in ML so nice. Also important are:

(0) Parametricity: Type variables are never case-analyzed. As a result, types convey useful information about what functions may or may not do. Haskellers call this “free theorems”. Java's `instanceof`, C++'s `sizeof` and template specialization, and GHC's `TypeFamilies` are blatant violations of parametricity that make types less informative.

(1) A clear distinction between data (sums of products) and operations (functions). In a general-purpose language, operations will always be somewhat ill-behaved: they may raise exceptions, fail to terminate, etc. Data tends to be better behaved, and algebraic laws can be stated about it, which hold even in the presence of effectful and/or non-terminating functions. This makes ML superior to Haskell, not to mention object-oriented languages.

(2) A module system that enforces abstraction boundaries between subsystems of a larger system. ML's opaque signature ascription (which has no counterpart in Haskell or object-oriented languages) ensures that the internal representation of abstract types is only visible in the module where they're implemented. In a well architected ML program, trying to violate another module's internal invariants is a type error!

> Static+strong typing is a nice combination, which is probably what hacker_9 meant to say.

That's a rather generous interpretation, given that hacker_9 said nothing about strong types, and instead made a claim about static vs. dynamic languages.

I do agree with your assertion, though; learning Haskell and OCaml prepared me for writing Python in ways that many of my peers in the Python community are unprepared. One big example is the difference between str and bytes in Python 3: a lot of Pythonistas find this distinction an annoyance, but I find it extremely useful, largely because I learned how to leverage such type differences to reduce errors from ML family languages.

I like the strong mission statement "it might be worth..."

His qualifying words make him sound weak and pensive. My money says he's not even a modern visionary/renaissance man.

I think Rust borrows enough from ML to give you the skill he is pointing at. Static types with plenty of places where type is inferred.

Rust is wonderful, but inference is actually one of its weakest points. It has only one feature that's incompatible with global inference (multiple types can have methods with the same name), but sadly that's enough to require you to manually annotate `Foo<Bar<Qux<T>>, Herp<Derp<U>>>`s in a lot of places. Rust arranges things so that these places are often, but not always, function type signatures.

In Haskell and ML, you can write tricky recursive functions without annotating a single type at all. Often, I couldn't even infer the type on my own in a reasonable amount of time! (By which I mean “under 5 seconds”, since my patience for these things is rather limited.) The type checker does it for me.

That's not been my experience so far, mind providing a more concrete example?

Only place I've had to annotate is when I'm using dynamic dispatch(&mut io::Write for instance) or collect() where I don't have enough information to determine type.

In Rust, function types need to be annotated. In Haskell or ML, I can have functions, especially recursive functions, with monstrous inferred types (although, of course, one then makes type synonyms for the sake of a more readable API) that would have to be explicitly annotated in Rust.

The reason why this isn't much of a problem for Rust programmers, is that idiomatic Rust code uses vectors and slices much more often than recursive data structures. But if you tried to roll your own recursive data structures, like those from Okasaki's book, you'd quickly feel the pain.

I like this about Rust. Functions (top-level, at the very least) should always have their types annotated, as it makes the code easier to read and understand. The fact that it makes type inference easier (does it?) for the compiler is just icing on the cake.

I consider myself to be a decent Haskell programmer and it has been a while since I wrote a function whose type I could not figure out. I suppose it is convenient to have the compiler be able to give you hints, especially when learning, but overall I find that when my types start getting really strange it's time to take a step back and see if there isn't a more straightforward way of doing it that'll lead to less headache down the road.

Also, I haven't dug into Rust that deeply but I've implemented some data structures for fun (working on an `Rc`-based rope with persistence right now) and I would not agree that working with types in Rust is fundamentally, significantly more onerous than in e.g. Haskell. There are other things that make implementing e.g. structures from the Okasaki book more difficult, like the need to work with the ownership model and various provided pointer types rather than simply relying on garbage collection.

> Functions (top-level, at the very least) should always have their types annotated, as it makes the code easier to read and understand.

I prefer to annotate definitions only at module boundaries, because that's precisely where an inferred type might be more general than what I actually want to expose. But not all functions are exported to other modules.

> I consider myself to be a decent Haskell programmer

Incidentally, Haskell's modularity story is very weak.

> and it has been a while since I wrote a function whose type I could not figure out.

Oh, I certainly have an idea of what type I'm expecting a top-level function to have when I define it. But I want the type checker help me write my program, not just confirm that what I've written is good. This is why, for example, GHC provides typed holes.

> but overall I find that when my types start getting really strange it's time to take a step back and see if there isn't a more straightforward way of doing it that'll lead to less headache down the road.

If everybody thought like that, then Haskell's `lens` and `pipes` libraries wouldn't exist, and that would be a great loss.

> Also, I haven't dug into Rust that deeply but I've implemented some data structures for fun (working on an `Rc`-based rope with persistence right now) and I would not agree that working with types in Rust is fundamentally, significantly more onerous than in e.g. Haskell.

No higher-kinded types or ML-style functors means that you can't:

(0) Parameterize recursive data structures over whether type recursion happens via `Box`, `Rc` or `Arc` pointers.

(1) Parametrically bootstrap complex data structures from simpler ones, Okasaki-style.

And no global type inference means that whatever little you can implement will be infinitely more verbose than its ML or Haskell counterpart.

Reply on news.ycombinator.com