35

我是依赖类型的新手，对两者之间的区别感到困惑。似乎人们通常说一种类型由另一种类型参数化并由某个值索引。但是在依赖类型语言中，类型和术语之间不是没有区别吗？参数和指数之间的区别是基本的吗？你能告诉我一些例子，说明它们在编程和定理证明中的含义不同吗？

4

2 回答 2

47

当您看到一系列类型时，您可能想知道它的每个参数是参数还是索引。

参数只是表示该类型有点通用，并且相对于提供的参数表现出参数化。

例如，这意味着无论您考虑哪种类型，该类型List T都将具有相同的形状： , ,等。 的选择仅影响可以插入, ,的值。Tnilcons t0 nilcons t1 (cons t2 nil)Tt0t1t2

另一方面，指数可能会影响您可以在该类型中找到哪些居民！这就是为什么我们说它们索引一个类型族，也就是说，每个索引都告诉你你正在查看哪个类型（在类型族中）（从这个意义上说，参数是所有索引指向的退化情况到同一组“形状”）。

例如，类型族Fin n或大小的有限集n包含非常不同的结构，具体取决于您对n.

索引0索引一个空集。索引1索引具有一个元素的集合。

从这个意义上说，指数价值的知识可能携带着重要的信息！通常，您可以通过查看索引来了解可能使用或未使用的构造函数。这就是依赖类型语言中的模式匹配如何消除不可行的模式，并从模式的触发中提取信息。

这就是为什么在定义归纳族时，通常可以为整个类型定义参数，但必须为每个构造函数指定索引（因为您可以为每个构造函数指定它所在的索引）。

例如我可以定义：

F (T : Type) : ℕ → Type
C1 : F T 0
C2 : F T 1
C3 : F T 0

这里，T是一个参数，而0和1是索引。当你收到一些x类型F T n时，看着是什么T也不会透露什么x。但是看看n会告诉你：

  • 必须x是C1或C3何时n是0
  • 那x一定是什么C2时候n1
  • 否则x一定是从矛盾中伪造出来的

同样，如果您收到 ay类型F T 0，您知道您只需要与C1and进行模式匹配C3。

于 2014-07-06T23:27:36.717 回答
1

这是一个由某个值参数化的类型的示例：

open import Data.Nat

infixr 4 _∷_

data ≤List (n : ℕ) : Set where
  []  : ≤List n
  _∷_ : {m : ℕ} -> m ≤ n -> ≤List n -> ≤List n

1≤3 : 1 ≤ 3
1≤3 = s≤s z≤n

3≤3 : 3 ≤ 3
3≤3 = s≤s (s≤s (s≤s z≤n))

example : ≤List 3
example = 3≤3 ∷ 1≤3 ∷ []

它是一种每个元素 less 或 equal 的列表n。一般的直觉是：如果某个类型的每个居民都有某些属性，那么您可以将其抽象为参数。还有一个机械规则：“如果每个构造函数在第一个索引位置（在结果类型中）具有相同的变量，则可以将第一个索引转换为新参数。” 此引用来自 *，您应该阅读它。

于 2014-07-06T23:25:20.450 回答