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

Ответ 1

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

• Как объясняется в разделе 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 # является числом без информации об ограничении размера) из числа не более я (что означает SNat i), возвращает число не более i; и для шаблона > в последней строке мы используем его для сопоставления с числом не более j, а тип рекурсивного вызова проверяется из-за подтипирования: SNat j ≤ SNat i.