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!

Functional programming for beginners

Happy New Year everyone; I hope you had a pleasant and relaxing festive holiday season. I sure did.

I’m starting the new year off by giving a short — an hour long or so — talk on how you can use ideas from functional programming languages in C#. It will broadcast this coming Wednesday, the 13th of January, at 10AM Pacific, 1PM Eastern.

The talk will be aimed straight at beginners who have some experience with OOP style in C# but no experience with functional languages. I’ll cover ways to avoid mutating variables and data structures, passing functions as data, how LINQ is functional, and some speculation on future features for C# 7.

There may also be funny pictures downloaded from the internet.

Probably it will be too basic for the majority of readers of this blog, but perhaps you have a friend or colleague interested in this topic.

Thanks once again to the nice people at InformIT who are sponsoring this talk. You can get all the details at their page:

http://www.informit.com/promotions/webcast-a-beginners-guide-to-functional-programming-141067

In related news, I am putting together what will be a very, very long indeed series of blog articles on functional programming, but not in C#. Comme c’est bizarre!

Foreshadowing: your sign of a quality blog. I’ll start posting… soon.

The dedoublifier, part four

I said last time that binary-searching the rationals (WOLOG between zero and one) for a particular fraction that is very close to a given double does not really work, because we end up with only fractions that have powers of two in the denominators. We already know what fraction with a power of two in the denominator is closest to our given double; itself!

But there is a way to binary-search the rationals between zero and one, as it turns out. Before we get into it, a quick refresher on how binary search works:
Continue reading

The dedoublifier, part three

All right, we have an arbitrary-precision rational arithmetic type now, so we can do arithmetic on fractions with confidence. Remember the problem I set out to explore here was: a double is actually a fraction whose denominator is a large power of two, so fractions which do not have powers of two in their denominators cannot be represented with full fidelity by a double. Now that we have this machinery we can see exactly what the representation error is:
Continue reading

The dedoublifier, part two

A couple of years ago I developed my own arbitrary precision natural number and integer mathematics types, just for fun and to illustrate how it could be done. I’m going to do the same for rational numbers here, but rather than using my integer type, I’ll just use the existing BigInteger type to represent the numerator and denominator. Either would do just fine.

Of course I could have used some existing BigRational types but for various reasons that I might go into in a future blog article, I decided it would be more interesting to simply write my own. Let’s get right to it; I’ll annotate the code as I go.
Continue reading

The dedoublifier, part one

Good Monday morning everyone; I hope my American readers had a lovely Thanksgiving. I sure did!

Well enough chit-chat, here’s a problem I was pondering the other day. We know that doubles introduce some “representation error” when trying to represent most numbers. The number 3/4, or 0.75 for example, can be exactly represented by a double, but the number 3/5, or 0.6, cannot.
Continue reading