Какие размеры в Агде?

Question

Какие размеры в Агде? Я пытался прочитать статью о MiniAgda, но не смог продолжить из-за следующих моментов:

1. Почему типы данных являются общими для их размера? Насколько я знаю, размер - это глубина дерева индукции.
2. Почему типы данных ковариантны относительно их размера, т.е. i <= j -> T_i <= T_j?
3. Что делать > а также # шаблоны означают?

Answer 1

1. Идея состоит в том, что размерный тип - это просто семейство типов, проиндексированных по размерам, которые по сути являются ординалами. При определении индуктивного типа как sized dataкомпилятор проверяет, что результатом является тип с правильным размером, так что, например, succ в SNat увеличивает размер в 1. Таким образом, для типоразмера S(i : Size) -> S i по сути элемент S с размером i, Мне кажется странным, почему определение нуля для SNat является zero : (i : Size) -> SNat ($ i) вместо чего-то вроде zero : (i : Size) -> SNat ($ 0),
2. Для размерных индуктивных типов это имеет смысл, поскольку T_i - это тип элементов T с размером меньше, чем i, так что если i ≤ j, то T_i ≤ T_j; Конструкторы должны увеличивать размер в рекурсивных вызовах.

3. Как объяснено в разделе 2.3, # эквивалентен T_∞, типу элементов T без ограничения по размеру; это верхний элемент для T_i в предзаказе подтипа. Шаблон (i > j) используется для привязки размера j при сохранении информации о том, что j

   fun minus : [i : Size] -> SNat i -> SNat # -> SNat i
   { minus i (zero (i > j)) y = zero j
   ; minus i x (zero .#) = x
   ; minus i (succ (i > j) x) (succ .# y) = minus j x y
   }
   

   Сначала подпись означает, что вычитая любое число (SNat # число без информации о размере) из числа не более i (вот что SNat i означает) возвращает число размером не более i; и для > pattern, в последней строке мы используем его, чтобы соответствовать количеству не более j, а рекурсивный тип вызова проверяется из-за подтипа: SNat j ≤ SNat i,