I wrote:
> > Can anyone explain to me what "first class structures" are,
> > and how they differ from (or relate to) existential types?
Thanks to everyone for the good explanations.
I have a couple more questions.
In my original question I had the quantifiers mixed up -- I thought
that "first class structures" sounded similar to existential types, but
as you have explained it is (locally quantified) universal types that
they are similar to.
So, is there any difference between "first class structures" and
locally quantified universal types?
The name "first class structures" seems to imply that the local
quantification is restricted to structures, and from a first
look at Jones' paper it seems that structures are a new language
construct. Now Haskell already has records and algebraic types.
Are structures any different from records, if we allow locally
universally quantified types in records? Is there any reason to
disallow locally universally quantified types in record types or
algebraic types?
Manuel Chakravarty wrote:
> To see the difference,
> consider the following data type definition:
>
> data Id a = AId (a -> a)
>
> Here we can construct for any arbitrary, but *fixed* `a' a value
> `AId f' where `f' is of type `a -> a'. In contrast, a structure of the
> form
>
> type Id = {id :: /\a. a -> a} -- let /\a. ... denote univ. quant. of `a'
Why did you switch from a `data' declaration to a record declaration here?
Couldn't we write
data Id = AId /\a . (a -> a)
?
--
Fergus Henderson <[EMAIL PROTECTED]> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger [EMAIL PROTECTED] | -- the last words of T. S. Garp.
