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

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 с размером меньше, чем я, так что, если я ≤ J, то T_i ≤ T_j; конструкторы должны увеличить размер в рекурсивных вызовах.

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

   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.