# Polymorphism and type inference

In this chapter, we’ll learn about defining type polymorphic functions, or how to work with generic types.

## 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
```

**Answer**

```
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
```

**Answer**

```
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.

Note

Program holes are a very powerful concept and form the basis of Meta-F*, the metaprogramming and tactics framework embedded in F*—we’ll see more about holes in a later section.

## 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.