[Agda] internal error with sized types

[Nils Anders Danielsson]

On 2009-02-12 09:44, Andreas Abel wrote:
> 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}

To be more concrete, note that you can define the following tree which
has unbounded depth:

 treeOfDepth1+ : ℕ → Tree
 treeOfDepth1+ zero    = leaf
 treeOfDepth1+ (suc n) = node (λ _ → treeOfDepth n)

 deep : Tree
 deep = node treeOfDepth1+

However, if the tree height were a natural number,

 data Tree : ℕ → Set where
   leaf : ∀ {n} → Tree (suc n)
   node : ∀ {n} → (ℕ → Tree n) →Tree (suc n)

then a tree analogous to deep would not be definable.

-- 
/NAD




This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.