[Agda] Positivity checker

[Nils Anders Danielsson]

On 2008-12-04 17:31, Wouter Swierstra wrote:
> 
> When I define the following data type in Agda, the positivity checker 
> complains:
> 
> data Data : Nat -> Set where
>   Base : Data Zero
>   Step : forall {n} -> (Data n -> Data n) -> Data (Succ n)
> 
> This declaration reeks of negativity, but on closer inspection it 
> shouldn't really be a problem. The index limits the amount of recursion 
> that can be done.

I argued in a similar way in "A Formalisation of a Dependently Typed
Language as an Inductive-Recursive Family".

> I suppose I could define a function into Set instead of a data type

Yes.

> but I'd much rather work with data (the example I have in mind is
> pretty complicated).

Yes.

> Is there a way to define this kind of data type without switching off 
> the positivity checker?

No. I suppose one could apply the termination checker to the type's
arguments, assuming that this does not interact badly with other things.

-- 
/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.