[Agda] Difference between two datatypes

[Sean Leather]

Hi,

On Fri, Jun 20, 2008 at 12:00, Wouter Swierstra <wss at cs.nott.ac.uk> wrote:

> 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,


Thanks, Wouter. That helps.

I was previously trying to align Set with Haskell types of kind * and Set1
types of kind * -> *, but it's obviously not that simple. Just to clarify
some terminology, would you say that 'X' is _parametrized by_ 'a' while Y is
_indexed over_ 'a'?

Thanks,
Sean
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080620/3318acb1/attachment.html