Dafny Power User: Type-Parameter Completion

K. Rustan M. Leino

Manuscript KRML 270, 22 June 2019

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.

# (opens new window)0. Type Parameters

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 (opens new window)

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

1. Examples

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 (opens new window)

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

2. Filling in Missing Type Arguments

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.

2.0. Example: One type parameter

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 (opens new window)

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>

2.1. Example: Two type parameters

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.

2.2. Example: Nested type parameters

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

2.3. Example: Datatype

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)

3. Auto-Declaring Type Parameters

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 (opens new window) above.

3.0. Examples

As we saw in Section 2.0 (opens new window) 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 (opens new window): 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>

3.1. Sometimes you need formal type parameters

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.

4. Final Notes

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. ↩ (opens new window)

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. ↩ (opens new window)

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. ↩ (opens new window)