[Agda] internal error with sized types

[Samuel Gélineau]

On Thu, Feb 12, 2009 at 4:44 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> The code you give below indexes data structures by natural numbers.
> You can always do so to add more information for the termination checker.

_More_ information? I thought Sized types were strictly more
expressive than Nat sizes, but I guess each must be useful in
different situations. This was the key cause of my misunderstanding.
Thanks for clearing that up!

> But sizes are the tree heights of data structures, which can be transfinite
> in case of infinitely branching trees.
>
> data Tree : {_ : Size} -> Set  where
>  leaf : forall {i} -> Tree {↑ i}
>  node : forall {i} -> (ℕ -> Tree {i}) -> Tree {↑ i}

I don't think I need transfiniteness for what I want to do, so that
settles it, then. I'll use Nat instead of Size.

In that Tree example, it seems that all we've accomplished using sized
types is to unify the type of trees with bounded height with the type
of trees with unbounded height. That might be useful when writing
transformations which are general enough to work on both, since we
won't have to duplicate the code. However, as soon as we encounter a
function for which we need to use sized types in order to show
termination, we need to split Tree into trees with bounded height
(Tree {i}) and trees with potentially unbounded height (Tree {∞}).

Representing bounded trees with (TreeFin : Nat -> Set) and unbounded
trees with (TreeInf : Set), it should be possible to prove that this
particular function terminates using Nat instead of Size. Sure, I
would need to write conversion routines from TreeFin {i} to TreeFin
{suc i}, and from TreeFin {i} to TreeInf, but I won't have to prove
size preservation lemmas or something; I will be able to show
termination using the same general strategy as if I was using sized
types.

So my newest question is: are sized types just a notational
convenience, or are there functions for which termination cannot be
proven without them, or at least without making the termination
argument much more complicated?

> Sized types offer you an unbounded size ∞ and subtyping wrt. sizes.

>From the examples in the slides of your "Sized Types in Agda"
presentation, I was under the impression that ∞ was mostly useful when
a termination argument didn't care about the size of a particular
argument. Using Nat, I represented (N ∞) as (∃ λ i → M i).

However, now I understand that ∞ means "of unbounded size", while (∃ λ
i → M i) means "of unknown yet finite size". To account for
unboundedness, let me generalize my non-magical size type S as
follows:

data SS : Bool → Set where
  z  : SS true
  s  : SS true → SS true
  ∞' : SS false

S : Set
S = SS true

⇑_ : {b : Bool} → SS b → SS b
⇑_ {true}  x  = s x
⇑_ {false} ∞' = ∞'

With this representation it is obviously not the case that (M i) is a
subtype of (M (⇑ i)) is a subtype of (M ∞'). However, for any datatype
following the convention of having all constructors return a value of
type (M (⇑ i)), it is straightforward to write coertion functions of
type (M i → M (⇑ i)) and (M i → M ∞'), to be used explicitly wherever
subtyping's implicit coercion would have been applied.

It seems to me that if sized types were implemented by translation, by
rewriting the program to use SS instead of Size, generating the
obvious coercion methods, and inserting them at the appropriate
places, we would get both the convenience of the sized type notation,
and the power of Nat or SS indices.

> The reason why "bla" has to be rejected is ∞, which matches against  ↑ i
>  with solution i = ∞.

I see! We need a way to tell Agda that in this particular function, I
do not expect i to be infinite.

Incidentally, with SS, the type of bla would be ({i : SS true} → M
{true} {i} → ⊤), and thus the value ∞' would not be an eligible
candidate for i, since it has type SS false instead of SS true.

hoping to improve the usefulness of sized types (which are already quite neat),
– Samuel