Polymorphism and type inference

Type: The type of types

One characteristic of F* (and many other dependently typed languages) is that it treats programs and their types uniformly, all within a single syntactic class. A type system in this style is sometimes called a Pure Type System or PTS.

In F* (as in other PTSs) types have types too, functions can take types as arguments and return types as results, etc. In particular, the type of a type is Type, e.g., bool : Type, int : Type, int -> int : Type etc. In fact, even Type has a type—as we’ll see when we learn about universes.

Parametric polymorphism or generics

Most modern typed languages provide a way to write programs with generic types. For instance, C# and Java provide generics, C++ has templates, and languages like OCaml and Haskell have several kinds of polymorphic types.

In F*, writing functions that are generic or polymorphic in types arises naturally as a special case of the arrow types that we have already learned about. For example, here’s a polymorphic identity function:

let id : a:Type -> a -> a = fun a x -> x

There are a several things to note here:

• The type of id is an arrow type, with two arguments. The first argument is a : Type; the second argument is a term of type a; and the result also has the same type a.

• The definition of id is a lambda term with two arguments a : Type (corresponding to the first argument type) and x : a. The function returns x—it’s an identity function on the second argument.

Just as with any function, you can write it instead like this:

let id (a:Type) (x:a) : a = x

To call id, one can apply it first to a type and then to a value of that type, as shown below.

let _ : bool = id bool true
let _ : bool = id bool false
let _ : int = id int (-1)
let _ : nat = id nat 17
let _ : string = id string "hello"
let _ : int -> int = id (int -> int) (id int)

We’ve defined a function that can be applied to a value x:a for any type a. The last line there maybe requires a second read: we instantiated id to int -> int and then applied it to id instantiated to int.

Exercises

Let’s try a few simple exercises. Click here for the exercise file.

Try defining functions with the following signatures:

val apply (a b:Type) (f:a -> b) : a -> b
val compose (a b c:Type) (f: b -> c) (g : a -> b) : a -> c

let apply a b f = fun x -> f x
let compose a b c f g = fun x -> f (g x)

How about writing down a signature for twice:

let twice a f x = compose a a a f f x

val twice (a:Type) (f: a -> a) (x:a) : a

It’s quite tedious to have to explicitly provide that first type argument to id. Implicit arguments and type inference will help, as we’ll see, next.

Type inference: Basics

Like many other languages in the tradition of Milner’s ML, type inference is a central component in F*’s design.

You may be used to type inference in other languages, where one can leave out type annotations (e.g., on variables, or when using type-polymorphic (aka generic) functions) and the compiler determines an appropriate type based on the surrounding program context. F*’s type inference includes such a feature, but is considerably more powerful. Like in other dependently typed language, F*’s inference engine is based on higher-order unification and can be used to infer arbitrary fragments of program text, not just type annotations on variables.

Let’s consider our simple example of the definition and use of the identity function again

let id (a:Type) (x:a) : a = x

let _ : bool = id bool true
let _ : bool = id bool false
let _ : int = id int (-1)
let _ : nat = id nat 17
let _ : string = id string "hello"
let _ : int -> int = id (int -> int) (id int)

Instead of explicitly providing that first type argument when applying id, one could write it as follows, replacing the type arguments with an underscore _.

let _ : bool = id _ true
let _ : bool = id _ false
let _ : int = id _ (-1)
let _ : nat = id _ 17
let _ : string = id _ "hello"
let _ : int -> int = id _ (id _)

The underscore symbols is a wildcard, or a hole in program, and it’s the job of the F* typechecker to fill in the hole.

Implicit arguments

Since it’s tedious to write an _ everywhere, F* has a notion of implicit arguments. That is, when defining a function, one can add annotations to indicate that certain arguments can be omitted at call sites and left for the typechecker to infer automatically.

For example, one could write

let id (#a:Type) (x:a) : a = x

decorating the first argument a with a #, to indicate that it is an implicit argument. Then at call sites, one can simply write:

let _ : bool = id true
let _ : bool = id false
let _ : int = id (-1)
let _ : nat = id 17
let _ : string = id "hello"
let _ : int -> int = id id

And F* will figure out instantiations for the missing first argument to id.

In some cases, it may be useful to actually provide an implicit argument explicitly, rather than relying on the F* to pick one. For example, one could write the following:

let _ = id #nat 0
let _ = id #(x:int{x == 0}) 0
let _ = id #(x:int{x <> 1}) 0

In each case, we provide the first argument of id explicitly, by preceding it with a # sign, which instructs F* to take the user’s term rather than generating a hole and trying to fill it.