Was sind Größen in Agda?

Question

Was sind Größen in Agda? Ich habe versucht, das Papier über MiniAgda zu lesen, aber nicht wegen der folgenden Punkte vor:

1. Warum sind Datentypen generic über ihre Größe? Soweit ich weiß, ist die Größe die Tiefe des Induktionsbaums.
2. Warum sind Datentypen kovariant über ihre Größe, d. H. I < = j -> T_i < = T_j?
3. Was bedeuten die Muster > und #?

Answer 1

1. Die Idee ist, dass eine Größe Art von Größen indizierten nur eine Familie von Typen ist, die im Wesentlichen ordinals sind. Bei der Definition eines induktiven Typs wie sized data prüft der Compiler, ob das Ergebnis ein Typ mit der richtigen Größe ist, sodass z. B. succ in die Größe in 1 erhöht. Auf diese Weise ist S(i : Size) -> S i im Wesentlichen ein Element von S mit der Größe i. Was mir komisch erscheint, ist, warum die Definition von Null für SNatzero : (i : Size) -> SNat ($ i) anstelle von etwas wie zero : (i : Size) -> SNat ($ 0) ist.
2. für geleimte induktive Typen ist dies sinnvoll, da T_i die Art der Elemente des T mit einer Größe von weniger als ist i, so dass, wenn i ≤ j ≤ dann T_i t_j; Konstruktoren müssen die Größe in rekursiven Aufrufen erhöhen.

3. Wie in Abschnitt 2.3 erläutert, ist # äquivalent zu T_∞, der Art von Elementen von T ohne bekannte Größengebundenheit; Dies ist ein Top-Element für die T_i in der Subtyping Preorder. Das Muster (i> j) wird verwendet, um eine Größe j zu binden, während die Information beibehalten wird, dass i. Das Beispiel in dem Papier für minus macht dies deutlich:

   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 
   } 
   

   Zuerst wird die Unterschrift bedeutet, dass Substraktion eine beliebige Anzahl (SNat # ist eine Zahl ohne Größe gebunden Informationen) aus einer Reihe von Größe höchstens i (das ist, was SNat i Mittel) gibt höchstens eine Größe zurück i; und für das > Muster, in der letzten Zeile verwenden wir es, um eine Zahl der Größe höchstens j zu entsprechen, und der rekursive Aufruftyp überprüft wegen der Subtypisierung: SNat j ≤ SNat i.