Excessive explanation, part two

We continue with my excessively detailed explanation of the seminal paper on the ML type inference system…

1 Introduction

This paper is concerned with the polymorphic type discipline of ML, 
which is a general purpose functional programming language, although 
it was first introduced as a metalanguage (whence its name) for 
constructing proofs in the LCF proof system. [4]

These bracketed numbers are not footnotes; they are references to other papers. See the original paper’s list of references if you want to follow up on these references.

By “type discipline” we basically mean the same thing as “type system”. That is, there is some way of determining the “type” of the expressions in a programming language, and detecting when the programs are erroneous due to violations of the typing rules.

By “polymorphic” here we mean what a C# programmer would mean by “generic”. There are many kinds of polymorphism in computer programming. “Subtype polymorphism” is what object-oriented programmers typically think of when someone says “polymorphism”:

void M(Animal a) { ... }
Giraffe g = new Giraffe();
M(g); // No problem.

That’s not the kind of polymorphism we’re talking about here. Rather, we’re talking about:

void N<T>(List<T> list) { ... }
List<int> g = ...;
N(g); // No problem.

This is often called “parametric polymorphism”, because the method takes a “type parameter”.

ML has parametric polymorphism, not subtype polymorphism.

A metalanguage is a language used to implement or describe another language. In this case, ML was first created to be the metalanguage for LCF, “Logic for Computable Functions”. The purpose of LCF was to automatically find proofs for mathematical theorems; you could write little programs in ML that described to the LCF system various strategies for trying to get a proof for a particular theorem from a set of premises. But as the paper notes, ML and its descendants are now general-purpose programming languages in their own right, not just implementation details of another language.

The type discipline was studied in [5] where it was shown to be 
semantically sound, in a sense made precise below, but where one 
important question was left open: does the type-checking algorithm — 
or more precisely the type assignment algorithm (since types 
are assigned by the compiler, and need not be mentioned by the 
programmer) — find the most general type possible for every expression 
and declaration?

As the paper notes, we’ll more formally define “sound” later. But the basic idea of soundness comes from logic. A logical deduction is valid if every conclusion follows logically from a premise. But an argument can be valid and come to a false conclusion. For example “All men are immortal; Socrates is a man; therefore Socrates is immortal” is valid, but not sound. The conclusion follows logically, but it follows logically from an incorrect premise. And of course an invalid argument can still reach a true conclusion that does not follow from the premises. A valid deduction with all true premises is sound.

Type systems are essentially systems of logical deduction. We would like to know that if a deduction is made about the type of an expression on the basis of some premises and logical rules, that we can rely on the soundness of those deductions.

The paper draws a bit of a hair-splitting distinction between a type checking algorithm and a type assignment algorithm. A type checking algorithm verifies that a program does not violate any of the rules of the type system, but does not say whether the types were added by the programmer as annotations, or whether the compiler deduced them. In ML, all types are deduced by the compiler using a type assignment algorithm. The question is whether the type assignment algorithm that the authors have in mind finds the most general type for expressions and function declarations.

By “most general” we mean that we want to avoid situations where, say, the compiler deduces “oh, this is a method that takes a list of integers and returns a list of integers”, when it should be deducing “this is a method that takes a list of T and returns a list of T for any T”. The latter is more general.

Why is this important? Well, suppose we deduce that a method takes a list of int when in fact it would be just as correct to say that it takes a list of T. If we deduce the former then a program which passes a list of strings is an error; if we deduce the latter then it is legal. We would like to make deductions that are not just sound, but also that allow the greatest possible number of correct programs to get the stamp of approval from the type system.

Here we answer the question in the affirmative, for the purely 
applicative part of ML. It follows immediately that it is decidable 
whether a program is well-typed, in contrast with the elegant and 
slightly more permissive type discipline of Coppo. [1]

This is a complicated one; we’ll deal with this paragraph in the next episode!

Excessive explanation, part one

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!

When would you use & on a bool?

UPDATE: A commenter points out that today is the 200th anniversary of the birth of George Boole; I had no idea when I scheduled this article that it would be so apropos. Happy birthday George Boole!

Here’s a little-known and seldom-used fact about C# operators: you can apply the & and | operators to bools, not just to integers. The & and | operators on bools differ from && and || in only one way: both operators always “eagerly” evaluate both operands. This is in marked contrast to the “lazily” computed evaluation of the && and || operators, which only evaluate their right hand argument if needed. Why on earth would you ever want to evaluate the right hand side if you didn’t need to? Why have this operation at all on bools?

A few reasons come to mind. First, sometimes you want to do two operations, and know whether both of them succeeded: Continue reading

Inferring from “is”, part two

In part one I gave a bunch of reasons to reject the proposed feature where the compiler infers additional type information about a local variable when inside the consequence of a conditional statement:

if (animal is Dog)
    // instead of ((Dog)animal).Bark();

But the problem still remains that this is a fairly common pattern, and that it seems weird that the compiler cannot make the necessary inference.

A number of readers anticipated my denouement and made some of the same proposals I was going to make in this part. Let’s go through a few of them; see the comments to the previous article for a few more.

Continue reading

Inferring from “is”, part one

In last week’s episode of FAIC I was discussing code of the form:

if (animal is Dog)

Specifically, why the cast was illegal if the variable tested was of generic parameter type. Today I want to take a bit of a different tack and examine the question “why do we need to insert a cast at all?” After all, the compiler should know that within the consequence of the if, the variable animal is guaranteed to be of type Dog. (And is guaranteed to be non-null!) Shouldn’t the code simply be:

if (animal is Dog)

Continue reading

Casts and type parameters do not mix

Here’s a question I’m asked occasionally:

void M<T>(T t) where T : Animal
  // This gives a compile-time error:
  if (t is Dog)
  // But this does not:
  if (t is Dog)
    (t as Dog).Bark();

What’s going on here? Why is the cast operator rejected? The reason illustrates yet again that the cast operator is super weird.
Continue reading

Nullable comparisons are weird

One of the C# oddities I noted in my recent article was that I find it odd that creating a numeric type with less-than, greater-than, and similar operators requires implementing a lot of redundant methods, methods whose values could be deduced by simply implementing a comparator. For an example of such, see my previous series of articles on implementing math from scratch.

A number of people commented that my scheme does not work in a world with nullable arithmetic (or, similarly, NaN semantics, which are similar enough that I’m not going to call out the subtle differences here.) That reminded me that I’d been intending for some time to point out that when it comes to comparison operators, nullable arithmetic is deeply weird. Check out this little program: Continue reading

Bottom ten list

Hey everyone, I am finally back from my many travels this summer and looking forward to doing some blogging this autumn. I’ll post some vacation photos when I have them sorted out. Until then, here’s an article that the nice people at InformIT asked me to write: what are my ten least favourite C# features?

I’m sure I missed some of your least favourites; I’d love to know what your pet peeves are in the comments here or on the article itself.