[Agda] Difference between two datatypes

[Wouter Swierstra]

On 20 Jun 2008, at 10:31, Nils Anders Danielsson wrote:

> On Thu, Jun 19, 2008 at 9:29 PM, Samuel Bronson <naesten at gmail.com>  
> wrote:
>>
>> I hope that gets fixed soonish... it's terribly annoying...
>
> In the last Agda Implementors' Meeting we discussed adding some form
> of universe polymorphism.

I should maybe point out that the "--type-in-type" flag solves all  
these  problems, although it does make your theory inconsistent.  
Writing out a universe by hand is usually not too much hassle for the  
programs I write - so this is really a last resort.

To answer Sean's original question though:

> data X (a : Set) : Set where
>   x : a -> X a
>
> data Y : Set -> Set1 where
>   y : {a : Set} -> a -> Y a

One way of explaining the difference between these two types is that X  
is a regular polymorphic Haskell data type (like lists); Y is a GADT.  
There are theoretical problems (similar to Russell's paradox and the  
set of all sets) to having "GADTs" in Agda that index over a Set. The  
solution is to have the data type "one level up" - in Set1. Indexing  
over Set1 gives a data type in Set2; etc. Hope this helps,

   Wouter

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.