主要观点：Dafny 支持 5 种类型参数变异性和基数保持模式，解释了这些模式及基数保持的需求，包括子类型、类型参数、声明变异性、正负位置、五种类型参数模式、内置类型构造函数的模式等内容，还提及了避免基数矛盾的相关规则和其他相关语言的处理方式。
关键信息：

• Dafny 中类型可被其他类型参数化，如Cell<Data>和datatype PS<X, Y>。
• 类型参数有协变、逆变、不变三种变异性，分别对应不同的子类型关系。
• 可通过前缀+、-、无标记来声明类型参数的变异性，且右值定义需与左值声明的变异性一致。
• 存在正负位置概念，用于判断类型参数的使用是否符合变异性。
• Dafny 有 5 种类型参数模式，包括默认的不变且基数保持模式等。
• 内置类型构造函数如set<+A>等有特定的类型参数模式。
• 为避免基数矛盾，需满足基数要求，即定义类型时要注意左右值的基数关系。
  重要细节：
• 如seq<nat>是seq<int>的子类型，而seq<bool>不是seq<real>的子类型，说明seq在其参数上是协变的。
• 以Coloring<X>为例说明逆变，每个Coloring<int>的值都是Coloring<nat>的值。
• 对于datatype等声明，可自由选择类型参数的变异性，若不一致可能导致逻辑矛盾。
• 用List的定义说明datatype构造函数在其参数上是单射的，且有逆函数（解构函数）。
• 通过F和D的类型声明及相关函数定义，展示了可能出现的基数矛盾及 Dafny 的处理方式。
• 介绍了基数要求的定义及在类型理论中的表示，以及如何通过标记来声明类型参数的基数保持性。
• 详细说明了内置类型构造函数如iset、map等的类型参数模式及其背后的原因和一些微妙的后果。