Strong Typing? It’s not really strong enough…

Maybe it’s just age, but I find myself slipping into being less and less tolerant of weak type-systems. Which may come as a surprise, given my involvement in TinyScheme, but I don’t see it as a contradiction. Scripting is a different kind of work than writing multi-module, complicated software, and it’s nice to be able to use a language that can express the Y combinator for the former. For the latter, though, I am becoming more and more autocratic. I want to deprive my programs from all freedom to do as they please. I frown when I see mission-critical software written in Python. I turn away when I see customer-facing software written in Perl. And I growl when I see big programs written in PHP. I’d lose sleep if I thought there were a place in my code ready to do something silly when I least expect it, “silly” being a synonym for “something a typechecker would catch right away”. And I’m not talking about preconditions, postconditions and assertions, because these will still take action at run-time. Although Bertrand Meyer’s Eiffel bringing them forth was very revolutionary, twenty-so years ago, given that they are not mainstream concepts even now. What I’m talking about, is incorporating more programmer intent into the type-system proper.

I want to introduce you to F* (F-Star) which you will find familiar-looking if you’re coming from F# (if you’re coming from Haskell, have a look at Agda, which covers similar ground). You can play with it on Rise4Fun through a simple browser without going into the trouble of installing anything. If you’re into .Net in general, have a look at Code Contracts, they are now being incorporated into the development ecosystem, so maybe they’ll become mainstream. It uses the same verification engine as F* (Z3), and it’s available right now (it has Code Contracts examples on Rise4Fun, as well). But I’m going to follow the F*/Agda direction in this post.

F* adds types of types (called kinds), so type constructors are typed (kinded) themselves. For example, “list” is actually a type constructor of kind * => *.

type list :: * => * =
   | Nil : 'a::* -> list 'a
   | Cons : 'a::* -> 'a -> list 'a -> list 'a

This is just a new point of view on usual functional notions. Here comes a new thing: term-indexed (or dependent) types. The following type is the length-indexed list, of kind int => * => *, meaning that it constructs a *-kinded type from an int-typed term and a *-kinded type.

type ilist :: int => * => * =
   | INil  : ilist 0 'a
   | ICons : x:'a -> n:int -> ilist n 'a -> ilist (n + 1) 'a

The real fun begins when you create functions of dependent types, like the following function to append two length-indexed lists (the Rise4Fun tutorial has these examples and more).

val iappend: n1:int -> ilist n1 'a -> n2:int -> ilist n2 'a -> ilist (n1 + n2) 'a
let rec iappend n1 l1 n2 l2 = match l1 with
   | INil -> l2
   | ICons x n1_minus_1 l1tl ->
     ICons x (n1_minus_1 + n2) (iappend n1_minus_1 l1tl n2 l2)

Something more is evident in the function signature, compared to that of a usual appending function. You can actually read, in the signature, the constraint that the length of the list this function produces is the sum of the lengths of its two list arguments. This is just a minimal example, and I’m afraid the full power of term-indexed types will not be evident to you from the F* tutorial alone. Material on Agda has more pointers to how on can embed propositional logic in dependent types. I hope you’re as excited as me with this prospect, which could sort-of merge what declarative constraints (like those on Code Contracts) can be expressed in the type-system itself, and functions will actually prove that what they’re doing has the intended properties, purely by doing type-correct operations!

Please go and play with the F* tutorial. It will not help you in your everyday job (but if you do have a job where F* can help you, please be kind enough to not tell me…), but it will open your mind to things that will come. When I was reading the Gentle Introduction to Haskell twenty years ago, I did not know that I’d be actually using F# and closures in C# twenty years hence.

But be prepared for a rough ride, because you won’t have the support you enjoy in the mainstream. For example, while trying to write the following function to map a length-indexed list to another, I stumbled on type errors, which, of course, is the idea.

val imap: n:int -> ('a -> 'b) -> ilist n 'a -> ilist n 'b
let rec imap (n:int) (f:'a->'b) (l1:ilist n 'a) = match l1 with
   | INil -> INil
   | ICons x n1 l1tl -> ICons (f x) n1 (imap n1 f l1tl)

Even so, getting errors like the following is not really helpful.

input(13,45-14,0) : Error : Expected an expression of type:

ILIST1.ilist x_11_2 'x_10_1

but got (x_13_2): ILIST1.ilist x_13_1 'x_10_1

Type checking failed: ILIST1

Well, that’s why it’s called the “bleeding edge”…