What are sized types in Agda?

Question

What are sized types in Agda? I've tried to read the paper about MiniAgda, but failed to proceed due to the following points:

1. Why are data types generic over their size? As far as I know the size is the depth of the tree of induction.
2. Why are data types covariant over their size, i.e. i <= j -> T_i <= T_j ?
3. What do the > and # patterns mean?

Answer 1

1. The idea is that a sized type is just a family of types indexed by sizes, which are essentially ordinals. When defining an inductive type as sized data, the compiler checks that the result is a type with the correct size, so that, for example, succ in SNat increases the size in 1. That way, for a sized type S (i : Size) -> S i is essentially an element of S with size i. What looks weird to me is why the definition of zero for SNat is zero : (i : Size) -> SNat ($ i) instead of something like zero : (i : Size) -> SNat ($ 0).
2. For sized inductive types this makes sense, as T_i is the type of elements of T with size less than i, so that if i ≤ j then T_i ≤ T_j; constructors must increase the size in recursive calls.

3. As explained in section 2.3, # is equivalent to T_∞, the type of elements of T with no known size bound; this is a top element for the T_i's in the subtyping preorder. The pattern (i > j) is used to bind a size j while keeping the information that j < i. The example in the paper for minus makes this clear:

   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
   }
   

   First the signature means that substracting any number (SNat # is a number with no size bound information) from a number of size at most i (that's what SNat i means) returns a number of size at most i; and for the > pattern, in the last line we use it to match a number of size at most j, and the recursive call type checks because of subtyping: SNat j ≤ SNat i.