Excessive explanation, part one

Posted on by

Well that was a long break! When I was studying for my Facebook interviews I realized that I was going to have no time to write in my blog if I got hired, so I wrote several dozen articles, batched them all up, and figured I would have plenty of time to write more by the time May rolled around. And then I did not! I have been crazy busy learning OCaml, learning Hack, and learning my way around Facebook systems. It’s been a huge amount of fun.

I would like to finish this series on designing and implementing a Z-machine in OCaml eventually, but I want to take a break from that for a bit and talk about another OCaml-related topic.

I frequently hear from readers and coworkers who don’t have a formal computer science theory background that they would love to learn more about programming languages, type systems, and so on, by reading papers. But that the academic papers are written in such a dense jargon that they bog down after the first couple of pages and can’t make further progress. That’s unfortunate. I thought what I might do is pick a short, seminal paper and go through it in excruciating detail over many episodes.

In my series on monads I gave particular emphasis to understanding monads via concepts familiar to professional C# programmers. I’m going to do the same in this series.

So without further ado…

Principal type-schemes for functional programs

Luis Damas † and Robin Milner
† The work of this author is supported by the Portuguese Instituto
Nacional de Investigacao Cientifica

First published in POPL ’82: Proceedings of the 9th ACM SIGPLAN-SIGACT
symposium on Principles of programming languages, ACM, pp. 207–212

Permission to copy without fee all or part of this material is granted
provided that the copies are not made or distributed for direct
commercial advantage, the ACM copyright notice and the title of its
publication and date appear, and notice is given that copying is by
permission of the Association for Computing Machinery. To copy
otherwise, or to republish, requires a fee and/or specific permission.
© 1982 ACM 0-89791-065-6/82/001/0207 $00.75

This is Damas and Milner’s seminal paper on how to do type inference in ML, the language that OCaml is based on.

We’ll more clearly define “type-scheme” later on, but briefly, by “type-scheme” we basically we mean what a C# programmer would mean by “method signature”. The goal here is to deduce the type signature of a method from its body. Of course, C# requires that you explicitly state the type of a method, and requires that you convert a lambda to a delegate of the appropriate type. In ML, these types are deduced, not manifest in the program text.

By “functional programs” we mean programs written in a functional style. Functional style emphasizes two things: immutability and treating functions as data. As we’ll see, the tiny little version of ML that this paper considers could be thought of as the “core” of a great many more complex functional languages.

Next time: The introduction!

12 thoughts on “Excessive explanation, part one”

  3. > “Ad hoc” polymorphism is what object-oriented programmers typically think of when someone says “polymorphism”

    “Ad hoc” polymorphism is what OO programmers call “overloading” (defining two functions with the same name, but different signatures). What you’re talking about (creating subclasses with modified behavior (overridden methods) and use those in place of instances of the superclass) is called “subtype polymorphism” in type theory.

    > I’ve asked a number of ML and Haskell experts why this is, and they usually say something about how it is “more natural” to say “string list”, but this is question-begging; it is only “more natural” because that’s what you’re used to seeing!

    In an English sentence “string list” is definitely more natural than “list string”, regardless of which programming languages you’re used to or whether you know any programming languages at all. “List string” simply makes no sense in the English language. Of course, you might quite reasonably object that “it looks more like valid English” is a misguided goal in programming language design and you wouldn’t be alone in feeling that way – my impression is that most function programmers prefer the order of “list string” – but either way that was the motivation of the ML designers.

    I also want to point out that Haskell actually uses “list string”, not “string list” for exactly the reason you pointed out (it’s like a function application at the type level). So, at least the Haskell programmers you were asking, weren’t used to the “string list” order.

    > VB solves the problem with “List of String”, which seems far more “natural” to me than “string list”.

    That’s a fair point – especially since ML (or OCaml at least) already uses the `of` keyword for the cases of data type definitions (`Cons of ‘a * ‘a list`), but maybe the designers felt using `of` for types would clutter the syntax too much or perhaps introduce some sort of ambiguity? Or maybe they just didn’t think of it.

    Reply ↓

  4. Am I going crazy or the article was edited? I thought I read like half of a very long version yesterday and today it is renamed to part 1 and is very short. The whole series was posted as one by error?

    Reply ↓

  5. Pingback: Easy methods to Handle Each Heroin Addiction Problem With Ease Using The following pointers - Pharm Tech Titans

Leave a comment