Разница между параметрами и индексами типа?

Я новичок в зависимых типах и смущен насчет разницы между ними. Кажется, люди обычно говорят, что тип параметризуется другим типом и индексируется некоторым значением. Но разве не существует различий между типами и терминами на языке с навязчивым типом? Является ли различие между параметрами и индексами фундаментальным? Можете ли вы показать мне примеры, показывающие разницу в их значениях как при программировании, так и при доказательстве теоремы?

Ответы

Ответ 1

Когда вы видите семейство типов, вы можете задаться вопросом, есть ли у каждого из аргументов параметры или индексы.

Параметры просто указывают на то, что тип несколько общий и ведет себя параметрически в отношении предоставленного аргумента.

Что это означает, что, например, в том, что типе List T будет иметь ту же форму, независимо от T вы считаете: nil, cons t0 nil, cons t1 (cons t2 nil) и т.д. Выбор T влияет только на значения, которые могут быть подключен к t0, t1, t2.

Индексы, с другой стороны, могут повлиять на жителей, которых вы можете найти в типе! Вот почему мы говорим, что они индексируют семейство типов, то есть каждый индекс сообщает вам, какой из типов (в пределах семейства типов) вы смотрите (в этом смысле параметр является вырожденным случаем, когда все индексы точки к одному и тому же набору "фигур").

Например, семейство типов 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 типа FT n, глядя на то, что T не обнаруживает ничего о x. Но, глядя на n вы скажете:

  • что x должен быть C1 или C3 когда n равно 0
  • что x должно быть C2 когда n равно 1
  • что x должен быть выкован из противоречия иначе

Аналогично, если вы получаете y типа FT 0, вы знаете, что вам нужно только совпадение шаблона с C1 и C3.

Ответ 2

Ниже приведен пример типа, параметризованного некоторым значением:

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 ∷ []

Это тип списков с каждым элементом меньше или равным n. Общая интуиция такова: если какое-либо свойство имеет место для каждого жителя типа, вы можете абстрагировать его на параметр. Существует также механическое правило: "Первый индекс можно превратить в новый параметр, если каждый конструктор имеет одну и ту же переменную в первой позиции индекса (в типе результата)". Эта цитата из *, вы должны прочитать ее.