Dafny Power User: Type-parameter modes: variance and cardinality preservation

K. Rustan M. Leino

Manuscript KRML 280, 9 August 2021

Abstract. Dafny supports 5 type-parameter variance and cardinality-preservation modes. Variance is common in languages with types, and cardinality preservation is a concern that arises in the context of verification. This note explains these modes and motivates the need for cardinality preservation. Along the way, it explains some phrases like “strict positivity”.

This note is long, so here's a little reading guide:

• If you're a beginner and want to learn about type-parameter variance, read the first 4 sections.
• If you're using type-parameter modes and are wondering about the syntax of each mode, see the table in Section 10 (opens new window).
• If you want to see which type-parameter modes are used with Dafny's built-in types, see Section 11 (opens new window).
• If you wonder what trouble you'd be in without cardinality-preservation rules (or, as some would say it, without “strict positivity”), then Section 7 (opens new window) will give you the idea (and the first code snippet in Section 9 (opens new window) adds type parameters to that example).
• If you're a language designer, you may find the rest of Section 11 (opens new window) to be food for thought.
• There's a little proof about finite powersets and cardinalities in Appendix A (opens new window).
• Finally, I have come to think that “strict positivity” is not a good term to use. I think “cardinality preservation” is more to the point, see Section 12 (opens new window).

0. Subtypes

Dafny defines a subtype relation on types. If A is a subtype of B, then every value of A is also a value of type B. For example, the subset type nat is a subtype of int. As another example, given

trait Tr {
  // ...
}
class Cl extends Tr {
  // ...
}

type Cl is a subtype of Tr.

Note. The definition of subtype above mentions “If”. This is not an “If and only if”, because it doesn't go the other way around. For example, the type

type Unreal = r: real | r == r + 1.0
  witness *

defines a type Unreal that has no values. Thus, every value of Unreal is also a value of int. Still, Dafny does not consider Unreal to be a subtype of int.

The subtype relation is reflexive—that is, every type is (trivially) a subtype of itself—and transitive. Other than that, there are three sources of subtyping in Dafny. One is that a subset type (like the built-in nat and the type Unreal above) is a subtype of its base type (int for nat and real for Unreal). Another is that a class or trait is a subtype of each trait it extends. For example, as we saw above, Cl is a subtype of Tr, and every reference type is a subtype of the built-in trait object (which, e.g., every class implicitly extends). The third source of subtyping stems from variance of type parameters, as I will explain in the next few sections.

1. Type parameters

A type can be parameterized by other types. For example,

class Cell<Data> {
  var data: Data
  // ...
}

introduces a class Cell parameterized by a type Data, and

datatype PS<X, Y> = PSCtor(x: X, ys: seq<Y>)

introduces a datatype PS parameterized by two types, where the values are essentially pairs consisting of one value (x) of the first type and a sequence (ys) of values of the other type.

Since Cell and PS have (1 and 2, respectively) type parameters, they sometimes known as (unary and binary) type constructors. This just means they are not types by themselves, but they need their parameters to be filled in to be types. For example, PS<int, real> and PS<bool, bool> are types, whereas PS<int> and PS are not.

Aside. In some cases, Dafny will fill in or infer the type arguments automatically. In those cases, you may be able to write just PS in your program. For example,

var p: PS := PSCtor(5, [3.14, 2.7]);

is a legal statement. This is just a syntactic shorthand, and the type arguments of PS are still there, even if the program text omits them.

2. Variance

Whether or not a parameterized type is a subtype of another may depend on the parameters. For example, it turns out that seq<nat> is a subtype of seq<int>, but seq<bool> is not a subtype of seq<real>. The reason behind this is that seq is co-variant in its argument.

2.0. Co-variance

When a (here, unary) type constructor M is co-variant in its argument, then

for any types A and B such that A is a subtype of B, M<A> is a subtype of M<B>.

Let me write the subtype relation as <:. Then, what I just said about M can be written as

A, B :: A <: B ==> M<A> <: M<B>

This is really just saying that M is monotonic (with respect to the subtyping ordering) in its argument. For example, in math, a function f over the reals is monotonic (with respect to the less-or-equal ordering) when

x, y :: x y ==> f(x) f(y)

A type constructor with many arguments may be co-variant in some of its type arguments and not others. For example, if Trois is a type constructor with three arguments and is co-variant in the first and third argument, then

A, B, H, X, Y :: A <: B && X <: Y ==> Trois<A, H, X> <: Trois<B, H, Y>

2.1. Contra-variance

Some type constructors are contra-variant in some of their type arguments. This means that the subtype of the argument has an opposite effect on the subtyping of the constructed type. More precisely, when a (here, unary) type constructor M is contra-variant in its argument, then

A, B :: A <: B ==> M<B> <: M<A>

This corresponds to the math notion of a function being anti-monotonic.

For illustration, consider the declarations

datatype Color = Blue | Green
type Coloring<X> = X -> Color

which, for any type X, defines Coloring<X> to be the type whose values are functions that give each X value a Color. As it turns out, type constructor Coloring is contra-variant in its argument. Consequently, every value of Coloring<int> is a value of Coloring<nat>. This makes sense—each value of Coloring<int> is a function that gives every integer a color, and each value of Coloring<nat> is a function that gives every non-negative integer a color, and every function that gives all integers a color also gives the non-negative integers a color.

2.2. Non-variance

For some type constructors, if you provide different type arguments, the resulting types have no relation to each other. For example, using class Cell from above, there is no subtype relation between Cell<nat> and Cell<int>. In this case, we say that the type constructor is non-variant in its argument.

Note. Perversely, non-variance is sometimes called invariance. That's a terrible mistake. “Invariant” refers to something that does not change, which is very much the opposite of the effect of non-variant type parameters. When you change the argument given to a non-variant type parameter, the resulting type can be something completely different—not the same thing. So, please… don't refer to non-variant as “invariant”!

3. Declaring variance

Dafny defines the type-parameter variance of the built-in type constructors. For example, seq is co-variant in its type argument. (I'll mention the other collection types in Section 11 (opens new window).) As another example, for any n, the n-ary arrow type constructor is contra-variant in each of its n input types and co-variant in its output type. Reference types (user-defined classes, built-in arrays, etc.) are required to be non-variant in each of their type parameters.

For datatype and codatatype declarations, subset types, opaque types, and type synonyms, there's some freedom in choosing the variance for each type parameter. To declare a type constructor to be co-variant in a type parameter, mark the type parameter with a prefix +. For contra-variance, mark the type parameter with a prefix -. The absence of any such mark declares the type constructor to be non-variant in that type parameter.

For example, the declaration

type Example<+A, -B, C, +D>

introduces an opaque-type type constructor Example with four type arguments. The type constructor is co-variant in its first and fourth arguments, contra-variant in its second argument, and non-variant in its third argument.

As another example, the built-in tuple type constructors (which are datatypes) are co-variant in each of their arguments.

Note. In Section 2.1 (opens new window), I said that Coloring<X> is contra-variant. That's not quite true. The right-hand side of the definition of Coloring<X> is contra-variant in X. If you want Coloring to have this property, you must explicitly mark the parameter as such. That is, Coloring<X> declared in 2.1 (opens new window) is non-variant in X, whereas declaring it as

type Coloring<-X> = X -> Color

makes it contra-variant.

There are no restrictions on the type-parameter variance of opaque types. But for the other type declarations, the right-hand side definition of the type must be consistent with each type-parameter variance given on the left-hand side.

For example, consider the following attempt at defining a datatype:

datatype Record<-X> = Record(x: X)  // error: X is not used contra-variantly

This declaration introduces X as a contra-variant type parameter of Record, but the right-hand side definition of Record does not use X according to that variance. If X is instead introduced as a co-variant or non-variant type parameter, the definition is legal.

Note. Even if the right-hand side is consistent with declaring a type parameter as co-variant or as contra-variant, the declaration of a type constructor does not need to advertise that to its users. In other words, it's fine to declare

datatype Record<X> = Record(x: X)

even though

datatype Record<+X> = Record(x: X)

is also legal and would allow more uses of Record. As another example, the Section 2.1 (opens new window) declaration of Coloring makes it non-variant, whereas its right-hand side would be consistent with making Coloring contra-variant. This is the same kind of choice of abstraction that is available throughout a programming language. For example, a function can have an int result type even it returns only non-negative integers. This establishes a contract between the implementation of a function and its callers. In particular, it says that the caller must be prepared to receive any integer result, and it gives the implementation the freedom to in the future return negative integers without breaking any callers.

4. Positive and negative positions

When looking at the right-hand side of a type declaration to see if the type parameters are used in accordance with their variance, it is useful to think of positive and negative positions. The basic idea is that an occurrence of a type X in a type expression T is in a positive position if the occurrence is to the left of an even number of arrows in T, and it is in a negative position if it occurs to the left of an odd number of arrows.

To illustrate, consider the following type expression:

(A, (B -> bool) -> C, seq<D -> (E -> F)>)

In this type expression, A, B, C, and F are in positive positions and D and E are in negative positions.

To explain the origin of the names “positive” and “negative”, let me write T(X) to denote a type expression where I have singled out a particular occurrence of X. If the X in T(X) occurs in a positive position, then any subtype/supertype change in X will cause a change in the same direction in T(X). That is, it is as if T(X) “multiplies” X by a positive number. Conversely, if X is in a negative position, then any subtype/supertype change in X will cause a change in the opposite direction in T(X). That is, it is as if T(X) “multiplies” X by a negative number.

In more symbols, if X occurs in a positive position in T(X), then

X, Y :: X <: Y ==> T(X) <: T(Y)

and if X occurs in a negative position in T(X), then

X, Y :: X <: Y ==> T(Y) <: T(X)

It's no accident that these formulas look like the ones that define co-variance and contra-variance in Section 2 (opens new window), because those concepts are tightly related to the concepts of positive and negative positions.

Consider a type-constructor declaration with a type parameter X and a right-hand side RHS. If X is marked as co-variant, then it is used correctly if all its occurrences in RHS are in positive positions. If X is marked as contra-variant, then it is used correctly if all its occurrences in RHS are in negative positions.

Let me tidy up a detail. In my above definitions of positive and negative positions, I only mentioned arrow type constructors. If for a moment we ignore syntax and write an arrow type like A -> B as Arrow<A, B>, then we can view the (built-in) definition of Arrow as

type Arrow<-X, +Y>

Now, the definition of positive/negative positions goes as follows. For any type T,

• If T has the form X where X is a type parameter, then this occurrence of X is in a positive position.

If

T

has the form

TC<..., U, ...>

where type expression

U

is passed in as the type parameter

A

in type constructor

TC

, then

• if A is declared as co-variant, then all the positive positions in U are positive positions in T and all negative positions in U are negative positions in T
• if A is declared as contra-variant, then all the positive positions in U are negative positions in T and all negative positions in U are positive positions in T
• if A is declared as non-variant, then U contributes neither positive nor negative positions to T

For example, in the type

seq<(A, Cell<B -> bool>, C -> D)> -> Example<int, E, F, G>

where Cell and Example are as defined above (and, recall, the built-in seq and the built-in tuple types are co-variant in their arguments, and the type constructor -> is like Arrow above), the type variables in positive positions are C and G, and the type variables in negative positions are A, D, and E.

5. Five type-parameter modes

In most programming languages that support type-parameter variance, you will encounter only the 3 modes of variance I've discussed so far. If that's all you want to know, you can stop reading now. (Dafny's defaults are such that you rarely need to know about more than these 3 modes.)

Dafny, it turns out, has 5 type-parameter modes. The additional modes come about because Dafny is concerned with formal verification. To motivate and explain the additional modes, I will review a property about datatypes, show a subtle way that mere type declarations can cause a logical contradiction, introduce the concept of cardinality preservation, and then come back to Dafny.

6. Injectivity

The constructors of a datatype or codatatype are injective in their arguments. This means that there is only one way to construct a particular datatype value.

In more detail, let's review four properties of datatypes. For illustration, let's consider a standard List definition (of integers—just to keep things simple).

datatype List = Nil | Cons(head: int, tail: List)

First, this definition says that there are two variants of lists: those that are constructed using Nil and those that are constructed using Cons. So, for any value xs of type List, the disjunction

xs.Nil? || xs.Cons?

always holds. Second, the two variants give rise to different values. So,

!(xs.Nil? && xs.Cons?)

always holds. Third, each constructor is a function, in the sense that its arguments (and nothing else!) determine the value they produce. So,

x == y && xs == ys  ==>  Cons(x, xs) == Cons(y, ys)

always holds. Fourth, two values of the same variant are equal only if the corresponding arguments are equal. So,

Cons(x, xs) == Cons(y, ys)  ==>  x == y && xs == ys

It's this fourth property that is called injectivity. More precisely, a datatype constructor is injective in each argument. (An alternate name for “injective” is “one-to-one”.) When a function is injective (in an argument), there exists an inverse function (for that argument). For a datatype, those inverse functions are called destructors, and they can be given names by introducing names for the parameters of the constructors. In the List declaration above, the inverse functions for Cons were introduced as .head and .tail. So, we have

Cons(x, xs).head == x  &&  Cons(x, xs).tail == xs

7. A logical contradiction

Consider the following type declarations:

type F = D -> bool
datatype D = Ctor(f: F)

I'm now going to argue that there is an infinite number of values of type D. Regardless of how many D values there are, we can define a function f``0 of type F that always returns false. If we pass in f``0 to Ctor, we get a D value, call it d``0. (We just proved that the set of D values is nonempty!) From our definition of f``0, we have that f``0``(d``0``) == false. Next, let's define a function f``1 that is like f``0, except that it returns true for d``0. Define d``1 to be the value Ctor(f``1``). Because f``0 is different from f``1, the injectivity of Ctor tells us that d``0 is different from d``1. (We have now shown that there are at least 2 D values!) Next, define a function f``2 that is like f``1, except that it returns true for d``1. By passing f``2 to Ctor, we get yet another D value. We can continue this process forever, which shows that there is no finite bound on the number of D values. Hence, the set of D values is infinite.

How many F values are there? If D were finite, you would immediately answer 2``|D|, where |D| is the size of D—also known as the cardinality of D—because for each D value, F may return one of 2 values. This is called the powerset of D. But as we just concluded above, D is infinite. Well, it turns out that the answer is still the same: the cardinality of F is 2``|D|, where we're using cardinal numbers instead of natural numbers. This sounds mathematical, but all you need to know is that the inequality n < 2``n holds for cardinal numbers just like it holds for natural numbers (see, e.g., Theorem 22.10 of [3 (opens new window)]). In other words, the number of F values is strictly larger than the number of D values.

This is trouble.

For every F value, we can construct a D value, and thus |F| <= |D|. But we concluded above that |D| < 2``|D| and 2``|D|`` == |F|. Putting these facts together by transitivity, we get |F| < |F|, which is just false.

Using a construction akin to Cantor's diagonalization argument [6 (opens new window)] or Russell's paradox [5 (opens new window)], we can exploit this contradiction in cardinalities and prove false:

lemma False()
  ensures false
{
  var g := (d: D) => !d.f(d);
  var dd := Ctor(g);
  calc {
    g(dd);
  ==  // def. g
    !dd.f(dd);
  ==  { assert dd.f == g; }
    !g(dd);
  }
}

Well, it's more accurate to say that this could be trouble, because it would let us prove false. Luckily, the type definitions for F and D are not accepted by Dafny. That is, to avoid this logical contradiction, Dafny does not allow a datatype (here, D) to be defined in terms of right-hand sides that would have larger cardinalities than D itself.

8. Cardinality requirement

To avoid the contradiction in cardinalities when defining a type D as some type expression T(D), we must make sure the cardinalities of D and T(D) can be the same. That is, we need to be able to make D large enough that its cardinality equals that of T(D). The previous section showed an example where this is not possible, because no matter how big you make D, T(D) will be exponentially larger. I'll refer to this condition as the cardinality requirement.

A contradiction in cardinalities can occur only if a type is defined in terms of itself. That is, suppose a type D is defined to be RHS. If RHS does not depend on D, then D will, without risk of any contradiction, have the same cardinality as RHS. A problem can occur only if RHS depends on D. For all cases of non-trivial dependencies, one can use an argument like in Section 7 (opens new window) to show that D has an infinite number of elements. Therefore, when designing a restriction to enforce the cardinality requirement, we only need to think about types of infinite cardinality.

In type theory, we can think of a fixed repertoire of type compositions. Types are either type names or sum-type, product-type, or arrow-type compositions. Type names include built-in types like bool and int, and also include user-defined types, like D from above. Sum types correspond to the variants of a datatype. Product types correspond to the list of arguments in each such variant. Finally, arrow types are the types of functions.

Using standard type-theory notation for these types and for the cardinality of the type named , the cardinality of types, denoted , is defined as follows:

From this definition, we see that the cardinality is a polynomial of the cardinalities of the type names involved, except in the case of arrow types. For any polynomial and infinite cardinal number , equals . So, the only way to violate the cardinality requirement is if D occurs in the left-hand argument of an arrow type.

Note. Just because D occurs in the left-hand argument to an arrow does not mean there is a problem with cardinalities. In particular, arrow types are harmless if the right-hand type has cardinality 0 or 1, and so are product types where an argument has cardinality 0. For example, Empty is an empty type (that is, a type with cardinality 0) and Singleton is a unit type (that is, a type with cardinality 1), then there is no cardinality concern with the type

datatype D = Done | More(D -> Empty, D -> Singleton, (D, Empty) -> int)

Nevertheless, Dafny's rules forbid this type, too, because the rules do not look for the special cases with cardinality-0 or cardinality-1 types. That's alright. By forbidding these trivial types, the rules both eliminate actual cardinality problems and stay simple.

The crucial point is this: Except for cardinality-0 types that are used as arguments to product types or as left-hand arguments to arrow types,

a type expression T(D) that mentions D is always at least as big as D.

This leads us to a proposed way to enforce the cardinality requirement:

For any type D defined to be T(D), do not allow D to be mentioned in the left-hand argument of any arrow type in T(D).

The proposed rule talks about left-hand arguments of arrow types, which reminds us of the positive/negative positions we discussed in Section 4 (opens new window) as a way to enforce variance restrictions. Some people think of the cardinality requirement as taking a step beyond saying D must be in positive positions. That is, whereas a doubly negative position (like X in (X -> bool) -> bool) is a positive position, the cardinality requirement seems to call for a strictly positive positions, where a doubly negative position is still a negative position. For this reason, you sometimes hear that the cardinality requirement is enforced by strict positivity. (I'll have more to say about this in Section 12 (opens new window).)

But wait! Weren't we discussing type parameters? What does the cardinality requirement have to do with type parameters?

9. Type parameters and cardinality

A variation of the example logical contradiction we saw in Section 7 (opens new window) can be written using type parameters:

type G<X> = X -> bool
datatype E = Ctor(g: G<E>)

Once the type synonym G is expanded, we get the same example, and indeed the same contradiction.

In a modular setting, it is not realistic to rely on being able to expand all types before checking for cardinality problems. For example, suppose type G is declared in a different module that exports G as an opaque type. A client module might then see just

type G<X>
datatype E = Ctor(g: G<E>)

from which it is not evident whether or not there may be problems with cardinality.

To solve this problem, Dafny lets every type constructor declare which of its type parameters are used in ways that preserve cardinality. The mark ! in the following example illustrates:

type Example<X, !Y>

This declaration says that Example uses type parameter X in a way that adheres to the cardinality requirement, whereas it does not promise the same for Y. This means that

datatype Good = None | Some(Example<Good, int>)

is legal, whereas

datatype Bad = None | Some(Example<int, Bad>) // error: violates cardinality requirement

is not, because it may violate the cardinality requirement.

We can now state the enforcement of the cardinality requirement precisely. Ignoring syntax, like I did in Section 4 (opens new window), we can view all types as type constructors that take a list of type parameters, each of which is identified as cardinality preserving or possibly not cardinality preserving. For any type T,

• If T has the form X where X is a type parameter, then this occurrence of X is a cardinality-preserving position iff X is marked as cardinality preserving.

If

T

has the form

TC<..., U, ...>

where type expression

U

is passed in as the type parameter

A

in type constructor

TC

, then

• if A is declared as cardinality preserving, then all the cardinality-preserving positions in U are cardinality-preserving positions in T
• if A is not declared as cardinality preserving, then U does not contribute any cardinality-preserving positions to T

The cardinality requirement is now enforced by the following cardinality-preservation rule: for any type D<..., X, ...> defined as RHS,

• In RHS, D is allowed to be used only in cardinality-preserving positions.
• If X is marked as cardinality preserving, then, in RHS, X is allowed to be used only in cardinality-preserving positions.

10. Combining variance and cardinality preservation

With 3 kinds of variance, each with cardinality preservation or not, you'd think we'd have 6 modes altogether. But there is no way to be contra-variant and cardinality preserving—in terms of arrow types, contra-variance says the type parameter is to the left of some arrow, and that makes it not preserve cardinality. Therefore, Dafny supports 5 modes. The default mode is non-variant, cardinality preserving. The other four modes can be indicated with the prefix marks +, *, -, and !, as shown by this table:

	cardinality preserving
variance	yes	not necessarily
co-variant	+	*
contra-variant	N/A	-
non-variant	(default)	!

11. Built-in type constructors

Dafny has several built-in type constructors. Here are their type-parameter modes:

set<+A>          // finite sets
iset<*A>         // possibly infinite sets
seq<+A>          // sequences
multiset<+A>     // multisets
map<+A, +B>      // finite maps
imap<*A, +B>     // possibly infinite maps
(+A, +B, +C)     // tuple types
-A -> +B         // arrow type for total functions
-A --> +B        // arrow type for partial functions
-A ~> +B         // arrow type for general functions
array<A>         // arrays
array2<A>        // multi-dimensional arrays

Most of these are probably what you'd expect. For example, as we have seen above in examples, sequences are co-variant in their type argument, and they are also cardinality preserving. Tuple types (a 3-tuple is shown above) are built-in datatypes and they are co-variant and cardinality-preserving in all their arguments. Array types of any dimension are reference types, which are restricted to be non-variant in their type parameters, and they are also cardinality preserving. Arrow types are co-variant and cardinality preserving in their last type parameter and, as we have discussed, contra-variant and not cardinality preserving in the other type parameters.

Some of type modes among the built-in types are more subtle. If you're tired of considering subtleties and are happy to accept the type-parameter modes of the built-in types, you can skip the rest of this section. If you want understand the rationale behind these type-parameter modes, keep reading.

11.0. iset and ->

An iset<X> is a possibly infinite set of X's. We can think of such a set as a function that for each X returns true or false, depending on whether or not the value is in the set. So, iset<X> is like the type X -> bool, which is not cardinality preserving in X.0 (opens new window) But why is iset<X> co-variant in X while X -> bool is contra-variant in X?

What I'm about to say applies to any types Y and X where Y is a subtype of X, but I find it helpful to think of specific, familiar types, so I will instead use the types nat and int.

Since nat is a subtype of int, co-variance would say that every iset<nat> value is also an iset<int> value. Indeed, a set containing only non-negative integers is also an iset<int>, so it makes sense that iset is co-variant in its type argument.

If -> were co-variant, then any nat -> bool function would have to be a int -> bool function, which isn't so. For example, consider the nat -> bool function

(n: nat) => 1000 / (n+1) < 20

This function evaluates to false for 3 and evaluates to true for 999. If we ignore the ": nat" type of the function's argument and try to think of the function as having type int -> bool, we expect to get a bool value if we apply the function to any integer. But the function's body is undefined for -1, so clearly it's not like an int -> bool function. We conclude that -> is not co-variant in its first argument.

Instead, it is contra-variant in its first argument. That is, every int -> bool function is also a nat -> bool function. Being the latter says you get a bool result whenever you apply it to a non-negative integer. Since that's also true for any int -> bool function, it makes sense to say -> is contra-variant in its first argument.

11.1. Two subtle consequences

There are two subtle consequences of the decision to make iset co-variant and _ -> bool contra-variant. They have to do with expressing membership/domain. To talk about them, let me first be explicit about the following principle in the Dafny language design:

• The Static Types Don't Alter Values principle.

  A static type says something about the value, but does not alter the value. If Y is a subtype of X, then you're allowed to assign a value of type Y to a variable of type X. In Dafny, such an assignment does not alter the value assigned. For example, given variables

  x: X    y: Y    originalY: Y
  

  the following assignments are allowed and result in the assertion being verified:

  originalY := y; // save the value of y
  x := y; // assign y to a variable of a different type (a supertype)
  y := x; // assign x back to y
  assert x == y == originalY;
  

  The assignment from y to x is allowed, since Y is a subtype of X. The assignment from x to y is allowed by the type system, but generates a proof obligation that the value of x at the time of the assignment is indeed a value of type Y. Since neither assignment alters the value, the final assertion succeeds.

Now, if s has type iset<int>, then the expression -7 in s evaluates to a boolean that tells us whether or not -7 is an element of set s. Suppose t has type iset<nat>. Is the expression -7 in t legal? Yes, because we could assign t to s (which, according to the language-design principle above, does not alter the value) and then ask -7 in s. Since there is a way to ask about -7's membership in t, it seems fine to allow the expression -7 in t directly, and that's what Dafny does.

Note. One could try to imagine a different language design, where an iset<int> value would be allowed to masquerade as an iset<nat> value. In such a language, consider the following program snippet, where variables s and t have types iset<int> and iset<nat>, respectively:

t := s;
assert s == t;
assert -7 in s <==> -7 in t;

By the Static Types Don't Alter Values principle, the first assertion should hold. And if s and t are indeed equal, then the next assertion should also hold. But that's nonsense, since every element of an iset<nat> is non-negative. Perhaps the language could outlaw the expression -7 in t, since -7 is not a value in the element type (nat) of the static type of t—but this doesn't help, since (as we considered above) we can ask about -7's membership in t without writing -7 in t directly. The conclusion is that such an imagined language design goes against the Static Types Don't Alter Values principle.

Next, if f is an int -> bool function, we can (by contra-variance) assign it to a variable g of type nat -> bool. Since f is defined on every integer, the expression f.requires(-7) is true. So what about g.requires(-7)? It would be strange for it to return true, since -7 is not a value of the first type parameter of g's type. But we also can't let it return false, because then g is not equal to f, which violates the Static Types Don't Alter Values principle. The only way out is to try to outlaw g.requires(-7).

For an expression e of static type A -> B, Dafny defines e.requires to have type A -> bool. So, f.requires has type int -> bool, which means one can pass -7 to it. But g.requires has type nat -> bool, so it is not legal to pass it -7.

11.2. set and iset

Having looked at iset<X> in detail, our first thought might be that set<X> would be the same. After all, we can view both iset<X> and set<X> as having values of the form X -> bool. While co-variance applies to iset and set alike, the cardinality concern we had with X -> bool and iset<X> does not apply to set<X> (explained next). Therefore, set's type parameter is declared with +.

For any type X, the values of iset<X> are in one-to-one correspondence with the powerset of X—that is, all functions from X to bool, or, equivalently, all possible subsets of X—whose cardinality is 2``|X|. The values of set<X> correspond to the finite powerset of X—that is, the functions from X to bool that return true only for a finite number of elements, or, equivalently, all finite subsets of X. The cardinality of the finite powerset is far smaller. Specifically, if X has infinite cardinality (which is the case we are interested in, see Section 8 (opens new window)), then the cardinality of the finite powerset of X equals the cardinality of X itself (see Appendix A (opens new window) for a proof).

11.3. map and imap

The last point to explain about the type-parameter modes of the built-in type constructors regards finite maps (map<X, Y>) and possibly infinite maps (imap<X, Y>).

You can view map<X, Y> and imap<X, Y> as (finite and possibly infinite) sets of pairs (x, y), with x a value of X and y a value of Y. Thus, as you consider subtypes (or supertypes) of either X or Y, the possible pairs shrink (or grow, respectively). This justifies the map types as being co-variant in both arguments.

Values of type imap<X, Y> are in one-to-one correspondence with the values of type X -> Y, so our concerns about cardinality preservation apply (hence, imap declares its first argument with the mark *). But the cardinality of map<X, Y>, which allows only a finite number of mappings from X to Y, is far smaller. So, analogously to set<X>, when X is infinite, map<X, Y> has no more elements than both |X| and |Y|.

12. Other sources

It seems that every textbook or course on types would cover the topic of cardinality preservation (or “strict positivity” as it's often called), but I have had difficulty finding such coverage. When I was first learning about this, the most useful reference I found was a seminal paper by Elsa Gunter [1 (opens new window)]. But even that paper left me puzzled as to what types a verification language can allow without the risk of a logical contradiction.

I now think that what had muddled my mind was the phrase “strict positivity”. I don't know who invented or popularized that phrase, but given the syntactic enforcement of cardinality preservation, I understand that it's tempting to think of the restriction as a stricter version of the positive-position restriction for type-parameter variance (Section 4 (opens new window)). But if you think of the requirement as barring a type name from occurring “to the left of any arrow”, then the motivation is not clear. “Positivity” has well established connotations with monotonicity, whereas “strict positivity” has nothing to do with monotonicity. Once you realize the salient point is how the cardinality of a type parameter affects the cardinality of the type generated by a type constructor, the light in your head comes on. If you—like I did—feel betrayed by the phrase “strict positivity”, you—like I do—will feel compelled to instead use the name cardinality preservation.

Many other verification languages incorporate restrictions to avoid logic contradictions. Of these, I want to mention the F* language [4 (opens new window)], which does not forbid types like those in Section 7 (opens new window); instead, to avoid logical contradictions, F* omits the injectivity property of constructors (see Section 6 (opens new window)) for such types. In other words, the constructors of a datatype in F* are injective only if the type satisfies the cardinality requirement.

13. Summary

Consider a (here, unary) type constructor T. Variance is a set of type-parameter modes that tell you what you can conclude about the subtyping relationship between T(X) and T(Y) by knowing something about the subtyping relationship between X and Y. Cardinality preservation is a set of type-parameter modes that tell you what you can conclude about the relative cardinalities of T(X) and T(Y) by knowing something about the relative cardinalities of X and Y. Dafny supports 5 type-parameter modes that a type constructor can use to express the desired combination of variance and cardinality preservation.

Acknowledgments

I first learned—years ago—about the logical contradiction in Section 7 (opens new window) from Jean-Christophe Filliâtre and Christine Paulin-Mohring.

Andreas Lochbihler demonstrated to me that the contradiction is detectable in Dafny, even though Dafny has no concepts or types that deal with cardinal numbers directly.

Discussions with Nik Swamy caused me to introduce the 5, not 3, type-parameter modes in Dafny, but I realize now that I was then still confused by the phrase “strict positivity”.

Recently, I had some illuminating discussions with Andrei Paskevich and Jatin Arora on this topic.

Remy Willems asked me questions about the type-parameter mark ! in Dafny, which prompted me to write this note to explore the topic in more detail. Little did I know I would spend this many words!

I'm grateful to all of these colleagues.

Dafny error message movie reference [0 (opens new window)].

References

[0]“Continuum Transfunctioner”. In Philip Stark, writer, and Danny Leiner, director, Dude, Where's My Car?, Twentieth Century Fox, Alcon Entertainment, 2000. 🔎 (opens new window)

[1]Elsa L. Gunter. Why we can't have SML-style datatype declarations in HOL. In Luc J. M. Claesen and Michael J. C. Gordon, editors, Higher Order Logic Theorem Proving and its Applications, Proceedings of the IFIP TC10/WG10.2 Workshop HOL'92., volume A-20 of IFIP Transactions, pages 561–568. North-Holland/Elsevier, September 1992. Preprint available at http://egunter.cs.illinois.edu/papers/HOL1992.pdf (opens new window). 🔎 (opens new window)

[2]Arturo Magidin. The cardinality of the set of all finite subsets of an infinite set. Math StackExchange, March 2011. https://math.stackexchange.com/questions/27096/the-cardinality-of-the-set-of-all-finite-subsets-of-an-infinite-set/27098#27098 (opens new window). 🔎 (opens new window)

[3]J. Donald Monk. Introduction to Set Theory. McGraw-Hill, 1969. Electronic version available from http://euclid.colorado.edu/~monkd/monk11.pdf (opens new window). 🔎 (opens new window)

[4]Nilhil Swamy, et al. F*: A higher-order effectful language designed for program verification. https://fstar-lang.org/ (opens new window). 🔎 (opens new window)

[5]Bertrand Russell. The Principles of Mathematics. W. W. Norton & Company, New York, 2d. ed. reprint edition, 1996. First published in 1903. 🔎 (opens new window)

[6]Keith Simmons. Universality and the Liar: An Essay on Truth and the Diagonal Argument. Cambridge University Press, 1993. ISBN 978-0-521-43069-2, https://www.google.com/books/edition/Universality_and_the_Liar/wEj3Spept0AC (opens new window). 🔎 (opens new window)

[7]chelivery. Cardinality of the set of all finite subset of . Math StackExchange, December 2016. https://math.stackexchange.com/questions/2057826/cardinality-of-the-set-of-all-finite-subset-of-mathbbr/2057908#2057908 (opens new window). 🔎 (opens new window)

A. Finite powerset preserves cardinality

While I haven't found the result in a textbook or journal article, math.stackexchange.com contains at least two proofs that finite powersets preserve cardinality [2 (opens new window), 7 (opens new window)]. Here's a version of [7 (opens new window)], but for any infinite set (not just ).

Theorem. Let be an infinite set and be the set of all finite subsets of . Then, .

Proof. To prove and to have the same cardinality, we need to show a bijection between the two. By the Schröder-Bernstein Theorem, it suffices to show an injective function from to and a (possibly different) surjective function from to . The function from each element in to the singleton set in is injective. So, it remains to show a surjective function from to .

For any natural number , let denote the -element subsets of . We then have that

Since, for each , is a subset of , there exists a surjective function . We define a function by . Function is surjective, because for any value in , , so by the surjectivity of there is an such that , and thus .

Alright, so we have a surjective function, , from to , but we need to show a surjective function from to . We have (see Section 8 (opens new window)), and and (since is infinite), so by cardinal arithmetic, . Hence, there is a surjective function, call it , from to . We conclude that is a surjective function from to , which completes our proof.

---

0.This had been defined incorrectly in Dafny. The issue (opens new window) was reported by Travis Hance and fixed (opens new window) by Jatin Arora. ↩ (opens new window)