Formal Methods
armchair_progamer
•
5mo ago
•
75%
Dafny Power User: Type-parameter modes: variance and cardinality preservation
https://leino.science/papers/krml280.htmlContext: Dafny is a programming language with a built-in SMT solver that can encode formally-checked statements (e.g. preconditions, postconditions, assertions).
Dafny has features of most programming languages; for example, covariant/contravariant/"non-variant" (invariant) type parameters. But in order to keep said verification sound and decidable in reasonable time, these features have extra restrictions and other complexities.
This article explains that there are 2 more "variance modes", because the of "covariant" and "invariant" variances may be "cardinality-preserving" or "not cardinality-preserving".
// Most "traditional" languages have 3 variances
type Foo<
+CovariantParameter,
NonVariantParameter,
-ContravariantParameter>
// Dafny has 5
type Bar<
+CovariantCardinalityPreservingParameter,
NonVariantCardinalityPreservingParameter,
-ContravariantParameter,
*CovariantNonCardinalityPreservingParameter,
!NonVariantNonCardinalityPreservingParameter>
Comments 0