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:
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.
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.
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.
When a (here, unary) type constructor M
is co-variant in its argument, then
for any types
A
andB
such thatA
is a subtype ofB
,M<A>
is a subtype ofM<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>
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.
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”!
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.)
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, 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 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 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.
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, 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
,
T
has the form X
where X
is a type parameter, then
this occurrence of X
is in a positive position.
T
has the form TC<..., U, ...>
where type expression U
is passed in as the
type parameter A
in type constructor TC
, then
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
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
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
.
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.
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
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]).
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] or
Russell's paradox [5], 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.
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 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 mentionsD
is always at least as big asD
.
This leads us to a proposed way to enforce the cardinality requirement:
For any type
D
defined to beT(D)
, do not allowD
to be mentioned in the left-hand argument of any arrow type inT(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
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.)
But wait! Weren't we discussing type parameters? What does the cardinality requirement have to do with type parameters?
A variation of the example logical contradiction we saw in Section 7 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,
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
,
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.
T
has the form TC<..., U, ...>
where type expression U
is passed in as the
type parameter A
in type constructor TC
, then
A
is declared as cardinality preserving, then all the cardinality-preserving
positions in U
are cardinality-preserving positions in T
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
,
RHS
, D
is allowed to be used only in cardinality-preserving positions.
X
is marked as cardinality preserving, then, in RHS
, X
is allowed to
be used only in cardinality-preserving positions.
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) | ! |
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.
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}
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.
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
.
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),
then the cardinality of the finite powerset of X
equals the cardinality of
X
itself (see Appendix A for a proof).
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|
.
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]. 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). 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], which does not forbid types like those in Section 7; instead, to avoid logical contradictions, F* omits the injectivity property of constructors (see Section 6) for such types. In other words, the constructors of a datatype in F* are injective only if the type satisfies the cardinality requirement.
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.
I first learned—years ago—about the logical contradiction in Section 7 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].
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, 7].
Here's a version of [7], 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), 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.