Skip to main content

System F is Amazing

I've been working with System F quite a bit lately, as it has a complicated enough typing system to be interesting, without having the full insanity of dependent types. I've been working with System F including sums products and recursive types. However, all of these can actually be encoded directly in System F. At first I thought this was merely a curiosity. It turns out however that for recursive types, the built in variety has some serious advantages.

System F allows you to take types as arguments as well as terms. From this system you can weave together an impressive array of very expressive types. First I'll define a few of these, and then I'll further describe what I find really fascinating.

The basic idea is that we can apply a function such as (Λ X . λ f : X→X, x : X. f x) to some types and terms and we evaluate in a way analogous to the λ-Calculus:

(Λ X . λ f : X→X, x : X. f x) [T] g t ⇒ g t

Now lets look at how we can spin some basic datatypes directly from such a simple calculus.

∀ X. X

This is the type 0. We can think of it as an encoding of False. It is a type which has no inhabitants. If we try to make one, we find we have no way to return a term of an arbitrary type X. Try filling in the question mark: Λ X. ?

0 → 0

This is the type 1. We can think of it as representing True. It has one inhabitant (that is, all terms that fill this type normalise to the same expression). It's fairly obvious how to write this one:

λ x:0. x

Now we'll move on to some standard language features in functional programming languages:

∀ X. (A→B→X) → X

This is the type of pairs (A,B). For any two types, A and B we can produce a pairing. The inhabitants of this are a bit more interesting:

pair :: ∀ A B. A→B→(A,B)
pair = Λ A B. λ a: A, b : B. Λ X. λ p : A→B→X. p x y

fst :: ∀ A B. (A,B)→A
fst = Λ A B. λ p : ∀ X. (A→B→X)→X . p [A] (λ x : A, y : B.x)

snd :: ∀ A B. (A,B)→B
snd = Λ A B. λ p : ∀ X. (A→B→X)→X . p [B] (λ x : A, y : B.y)

The constructors and destructors just fall out naturally. You hardly have to think at all about what to produce, just follow the type discipline. This is part of the beauty of parametricity.

∀ X. (A→X)→(B→X)→X

This is the type of sums A+B. If you look closely, you'll see that there is a pattern developing. Constructors for a datatype have the form (K1→...→X). See if the pattern is more obvious from the code below.

inl :: ∀ A B . A→A+B
inl = Λ A B . λ a:A. Λ X . λ left : A→X, right B→X. left a

inr :: ∀ A B . B→A+B
inr = Λ A B . λ b:B. Λ X . λ left : A→X, right B→X. right b

case :: ∀ A B C. A+B→(A→C)→(B→C)→C
case = Λ A B C. 
              λ c : ∀ X. (A→X)→(B→X)→X.
                λ f: A→C, g:B→C
                        c [C] f g

If you look closely at the way case was defined, you'll see that we didn't actually do anything. It turns out that inhabitants of the data act as their own case selector. If you try writing down Bool:

∀ X. X→X→X

You'll find a similar thing is true for if-then-else, which turns out to be superfluous. This is great! So we can get "case" for free from the data type. It turns out this works in general for inductive types.

Now, for something really amazing. It turns out that recursive types are present as well. The data type Nat, which is often written as μ X. 1+X, can be written down as follows:

∀ X. X→(X→X)→X

If you've been paying attention, you'll note the correspondence between the first X and Zero, and the second (X→X) and Succ. Well it turns out μ X. F X can be encode itself as follows:

μ X. F X = ∀ X. (F X→X)→X

Ok great. That's fairly interesting. Now comes the part that had me floored with the beauty of System F. It is typical in programming languages to have an explicit constructor which allows us to inject into a type. For fun we can write the following type, which simulates the domain equation of the untyped lambda calculus:

data D = InD D→D

This turns out to be somewhat interesting, in that we can produce non-terminating computations with the type, without ever using explicit recursion. Witness the following code*:

omega = (\ x -> case x of 
                     InD g -> g (InD g))
               (InD (\ x -> case x of 
                         InD g -> g (InD g)))

Great! We can write down silly terms that don't terminate. What's the point you ask? Well, we can write down this type in System F. But System F is strongly normalising (it will always evaluate to a normal form, so it can't just compute forever). Something seems fishy here, how can this possibly be? Let us look at this datatype in System F.

∀ X . (X→X)→X

So far so good. Now, let's try to make the constructor:

omega = Λ X . λ f : X→X. ???

We can't find one! What happened? It turns out that this type is not inhabited in System F. When we wrote the constructor in Haskell, we were LYING!!! That constructor doesn't actually exist, because that type has no valid inhabitants.

It's often the case that in proof assistants recursive types are restricted, often with a positivity restriction on the functor F such that such we don't end up lying about what constructors are actually possible. However, in System F, where we are asked to provide the constructors, this problem never occurs. It seems likely to me that since Mendler style induction schemes are more general than induction with functors restricted to positivity, that there are many types which have inhabitants in System F, which are thrown out by proof assistants such as Coq, despite being perfectly O.K. In addition, there are all sorts of silly types that are allowed in a language like Haskell, despite the fact that they have no realistic inhabitants.

I hope you found this as amazing as I did.

* Note: you might have to add some arbitrary show instance to get haskell to allow you run omega. Don't worry about how you define "show" since omega never returns!

Comments

Popular posts from this blog

Decidable Equality in Agda

So I've been playing with typing various things in System-F which previously I had left with auxiliary well-formedness conditions. This includes substitutions and contexts, both of which are interesting to have well typed versions of. Since I've been learning Agda, it seemed sensible to carry out this work in that language, as there is nothing like a problem to help you learn a language.

In the course of proving properties, I ran into the age old problem of showing that equivalence is decidable between two objects. In this particular case, I need to be able to show the decidability of equality over types in System F in order to have formation rules for variable contexts. We'd like a context Γ to have (x:A) only if (x:B) does not occur in Γ when (A ≠ B). For us to have statements about whether two types are equal or not, we're going to need to be able to decide if that's true using a terminating procedure.

And so we arrive at our story. In Coq, equality is som…

Formalisation of Tables in a Dependent Language

I've had an idea kicking about in my head for a while of making query plans explicit in SQL in such a way that one can be assured that the query plan corresponds to the SQL statement desired. The idea is something like a Curry-Howard in a relational setting. One could infer the plan from the SQL, the SQL from the plan, or do a sort of "type-checking" to make sure that the plan corresponds to the SQL.

The devil is always in the details however. When I started looking at the primitives that I would need, it turns out that the low level table joining operations are actually not that far from primitive SQL statement themselves. I decided to go ahead and formalise some of what would be necessary in Agda in order get a better feel for the types of objects I would need and the laws which would be required to demonstrate that a plan corresponded with a statement.

Dependent types are very powerful and give you plenty of rope to hang yourself. It's always something of…

Plotkin, the LGG and the MGU

Legend has it that a million years ago Plotkin was talking to his professor Popplestone, who said that unification (finding the most general unifier or the MGU) might have an interesting dual, and that Plotkin should find it. It turns out that the dual *is* interesting and it is known as the Least General Generalisation (LGG). Plotkin apparently described both the LGG for terms, and for clauses. I say apparently because I can't find his paper on-line.

The LGG for clauses is more complicated so we'll get back to it after we look at the LGG of terms. We can see how the MGU is related to the LGG by looking at a couple of examples and the above image. We use the prolog convention that function symbols start with lower case, and variables start with uppercase. The image above is organised as a DAG (Directed Acyclic Graph). DAGs are a very important structure in mathematics since DAGs are lattices.

Essentially what we have done is drawn an (incomplete) Hasse diagram f…