[Agda] Difference between two datatypes

[Wouter Swierstra]

On 20 Jun 2008, at 13:35, Sean Leather wrote:

> would you say that 'X' is _parametrized by_ 'a' while Y is _indexed  
> over_ 'a'?

Yes - that's exactly it.

Set (roughly) corresponds to Haskell's *; Set1 is the kind of Set;  
Set2 is the kind of Set1; etc.

There are a few places where this doesn't quite line up. For example,  
in Haskell you can write:

   data NatTrans f g where
     NatTrans :: forall a . f a -> g a

That is, you define a data type with a polymorphic constructor. The  
corresponding Agda data type would necessarily live in Set1.

Here's a bad attempt at explaining why the Haskell version is  
logically dubious: the NatTrans data type defines a new type; yet the  
constructor quantifies over *all* types, including NatTrans, which you  
were trying to define to begin with. Definitions like NatTrans are  
called "impredicative" - I'm not sure if they necessarily lead to an  
inconsistent theory (like Set : Set does), but they do complicate the  
metatheory and are generally frowned upon by people who know much more  
type theory than I do. Best,

   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.