Dafny Power User:

Type-Parameter Completion

Type-Parameter Completion

**Abstract.** When type parameters don't need to be named, Dafny has a scheme for filling
them in automatically. Omitting the type parameters reduces clutter in
function signatures. This note describes how the type parameters get filled in.

As in many languages, types in Dafny can be parameterized by other types.
For example, the type `set<int>`

denotes finite sets of integers and is
parameterized by `int`

. As another example, if `List`

is a type defined as

`datatype List<A> = Nil | Cons(A, List<A>)`

and `Expr`

is a type denoting expressions, then `List<Expr>`

is a type that is parameterized by `Expr`

. In the declaration of `List`

,
`A`

is a *formal* type parameter, and in the type `List<Expr>`

, `Expr`

is
the *actual* type parameter (or, actual type argument).

Since `set`

and `List`

each requires a type parameter, they are not
themselves types. That is, it doesn't make sense for a variable to have
type `set`

. We say that `set`

and `List`

are *type constructors*. More
precisely, they are *unary* type constructors, since they take one type
parameter. Each type constructor has an *arity*, which says how many type
parameters it needs. So, a unary type constructor has arity 1. (There
are no type constructors with arity 0; such a thing is simply a type.)

In Dafny, type constructors are not first class. This means that every mention of a type constructor must always be fully instantiated. However, the instantiation need not be explicit in the program text.

In the signature declarations of datatypes, functions, and methods, Dafny
allows type constructors to be used without explicit type parameters.
In this note, I describe Dafny's scheme for filling in those missing
type parameters.^{0}

Let's start by looking at two examples that show the advantages of having such a scheme.

Here are functions for computing the length of a list and for computing the set of elements in a list.

```
function method Length(list: List): nat {
match list
case Nil => 0
case Cons(_, tail) => 1 + Length(tail)
}
function method Elements(list: List): set {
match list
case Nil => {}
case Cons(x, tail) => {x} + Elements(tail)
}
```

At first glance, they look to be exactly what you expect. But if you
think some more, you will notice that `List`

and `set`

have no given type
parameters. This is delightful! Both `Length`

and `Elements`

have more
to do with the structure of the list than with the types of the elements
stored in the list, and therefore it's nice that the definitions of
these functions don't need to be cluttered up with the declaration
and uses of the type parameters.

If you wrote the type parameters explicitly, the signatures of the functions above would look like this:

```
function method Length<A>(list: List<A>): nat
function method Elements<A>(list: List<A>): set<A>
```

You'll agree this is rather heavy on the `<A>`

's.^{1}

So that you can use these abridged signatures effectively, let's now look at how omitted type parameters are filled in.

In the *type signatures* of functions and methods and in the *right-hand side* of
(the "`=`

" in) datatype definitions, type parameters can be omitted.
The rule is that if the type signature or
right-hand side mentions a type constructor without any type
arguments, then Dafny will fill these in from a
*prefix of the formal type parameters* of the enclosing function, method,
or datatype.

Suppose the program text includes the following function signature:

`function method ReverseAux<``A`

>(list: List<A>, acc: List): List<A>

`<A>`

Note that `List`

in the type of `acc`

does not have an explicit type
argument. Dafny now fills in the type parameter of `List`

using the type
parameter of function `ReverseAux`

, completing the type of `acc`

`List<A>`

,
as illustrated by the arrow above.^{2}

The type arguments to the other occurrences of `List`

in the function's type signature
can be filled in in the same manner. So, the same function `ReverseAux`

can
be declared simply as:

`function method ReverseAux<``A`

>(list: List, acc: List): List

`<A>`

`<A>`

`<A>`

Consider a datatype `Path`

with two type parameters:

`datatype Path<L,R> = Stop | Left(L, Path<L,R>) | Right(R, Path<L,R>)`

A value of type `Path<L,R>`

represents a finite path of left- and right-turns.
Each left-step is accompanied by a value (call it a “breadcrumb”, if you wish)
of type `L`

and every right-step is accompanied by a breadcrumb of type `R`

.

Here are two functions on paths. `Hansel`

picks up all the breadcrumbs
encountered on left turns and `Gretel`

picks up all the breadcrumbs
encountered on right turns.

```
function Hansel<L,R>(p: Path<L,R>): List<L> {
match p
case Stop => Nil
case Left(l, rest) => Cons(l, Hansel(rest))
case Right(_, rest) => Hansel(rest)
}
function Gretel<L,R>(p: Path<L,R>): List<R> {
match p
case Stop => Nil
case Left(_, rest) => Gretel(rest)
case Right(r, rest) => Cons(r, Gretel(rest))
}
```

Using Dafny's type-parameter completion, we can write these as:

`datatype Path<L``,`

R> = Stop | Left(L, Path) | Right(R, Path)
function Hansel<L`,`

R>(p: Path): List
function Gretel<L`,`

R>(p: Path): List<R>

`<L,R>`

`<L,R>`

`<L,R>`

`<L>`

`<L,R>`

Note that both occurrences of `Path`

in the right-hand side of the declaration
of type `Path`

get both type arguments filled in with the type's type
parameters `<L,R>`

given in the left-hand side of the declaration. In both of
the functions, `Path`

also gets the arguments `<L,R>`

as declared
in the functions. Moreover, for `Hansel`

, type `List`

automatically gets the
argument `<L>`

, because `List`

needs one argument and therefore it only picks
up a prefix of the function's type parameters `<L,R>`

. Function `Gretel`

has result type `List<R>`

. Here, it is not possible to elide the type
argument list `<R>`

, since `<R>`

is not a prefix of `<L,R>`

.

The example illustrates how type-parameter completion picks a prefix of
the enclosing function's type parameters. This allows you to write just
`List`

instead of `List<L>`

. However, since `L`

and `R`

otherwise play
symmetric roles in this example, you can of course also choose to write
out `List<L>`

explicitly. You may argue that doing so more clearly highlights
the difference between functions `Hansel`

and `Gretel`

. You would then
write the following signatures:

```
datatype Path<L,R> = Stop | Left(L, Path) | Right(R, Path)
function Hansel<L,R>(p: Path): List<L>
function Gretel<L,R>(p: Path): List<R>
```

which still looks pretty clean.

Type-parameter completion applies not just to the outermost types. For example,

`datatype Tree<A> = Node(children: List<Tree<A>>)`

can also be written as

`datatype Tree<``A`

> = Node(children: List<Tree>)

`<A>`

Note that if you supply any type parameters at all, then Dafny will not change or complete the list you have given. The completion rule supplies the parameters to a type constructor only if the type constructor is mentioned with no type arguments at all (that is, without any angle brackets).

Type-parameter completion also applies in the right-hand side of datatypes.
So, if you want to, you can declare `List`

as follows:

`datatype List<A> = Nil | Cons(A, List)`

What I described so far pertains to the *actual* type arguments of
type constructors in signatures. There's one more part to Dafny's
type-parameter completion. For functions and methods, but not for datatypes,
if the function or method is declared without explicit *formal* type parameters,
then Dafny provides these as well. This list of formal type parameters
in this completion will be made long enough to
cover the length of any missing type-argument list described in
Section 2 above.

As we saw in Section 2.0 above,
function `ReverseAux`

can omit the uses of its type parameter `A`

.
Consequently, there is no need for the signature to mention `A`

by name.
Dafny's type-parameter auto-declaration rule allows us to omit `A`

altogether. By doing so, we can declare `ReverseAux`

simply as

```
function method ReverseAux(list: List, acc: List): List
```

`<A>`

`<A>`

`<A>`

This declaration says that `ReverseAux`

takes two lists and returns a list.
There's no need to explicitly mention the type of list elements, and it
is tacitly understood that the three lists mentioned have the same type
of elements.

We already saw two other examples in the motivational Section 3.0:
`Length`

and `Elements`

. Function `Elements`

relies on type-parameter
completion in three ways: both the user-defined type constructor `List`

and the built-in type constructor `set`

are completed with the same
type parameter and this (un-named) type parameter is added to the formal
type parameters of the function.

```
function method Elements(list: List): set
```

`<A>`

`<A>`

Note that you cannot take advantage of the auto-declaration part of
type-parameter completion if you have a need to mention
the type parameter. For example, you can shorten the signature of `Snoc`

to:

```
function method Snoc<A>(list: List, a: A): List {
match list
case Nil => Cons(a, Nil)
case Cons(x, tail) => Cons(x, Snoc(tail, a))
}
```

But since `a`

's type needs to be mentioned as `A`

, you must declare
`A`

explicitly. That is, you cannot abbreviate `Snoc`

's type signature
more than this.

Actual type parameters are completed in the right-hand side of
datatype declarations, but auto-declaration of formal type parameters
does not apply to datatypes. For example, you cannot omit the
`<A>`

in the left-hand side of the declaration of `List`

.

Recall that if you supply any type parameters at all, then Dafny will not extend the list you have given. The completion rule will supply type parameters to a function or method only if the function or method is declared with no type parameters at all (that is, without any angle brackets).

Finally, remember that Dafny's type-parameter completion is a feature, not a requirement. If you don't want to make use of this completion, then by all means, feel free to write out all formal type parameters and actual type arguments explicitly in your own programs.

^{0.}Dafny's scheme for filling in type parameters in signature declarations
is one of two mechanisms that the language employs to reduce type
clutter in the program text. The other mechanism is *type inference*,
which tries to figure out types of variables and expressions based on
how these are *used*. In this Power note, I will not talk about type
inference.
↩

^{1.}The compiled function `Elements`

makes use of one other thing that
Dafny fills in automatically, namely the fact that the argument to
`set`

needs to be a type that supports equality in compiled contexts.
If you wrote this explicitly, the function signature would be

`function method Elements<A(==)>(list: List<A>): set<A>`

In this note, I won't say more about equality-supporting types or how Dafny tries to infer these. ↩

^{2.}The Dafny IDE in Visual Studio displays type information in tool tips.
If you hover the mouse over `acc`

in this IDE, the tool tip that pops
up will tell you the full type of `acc`

, namely `List<A>`

.
In the future, the other Dafny IDEs may also show such type tool-tips.
↩