> Fergus Henderson writes:
>
> > > 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.
Yes, but existential quantificaton can be modelled by universal
quantification by applying a continuation passing transform:
ex t. T ~~~ all r. (all t. T -> r) -> r
Hence, first class structures (in the sense you mean the term) give
you the power of existential types, at the price of an encoding. This
is explained in more detail in a paper from last POPL:
@InProceedings{odersky-laufer:annotations-conf,
author = {Martin Odersky and Konstantin L\"aufer},
title = "Putting Type Annotations To Work",
booktitle = "Proc. 23rd ACM Symposium on Principles of
Programming Languages",
year = 1996,
month = jan,
pages = 65-67
URL = http://wwwipd.ira.uka.de/~odersky/papers.html/#Types
}
-- Martin Odersky
======================================================================
Prof. Martin Odersky e-mail: [EMAIL PROTECTED]
Department of Computer Science Tel: +49 721 608 3495
University of Karlsruhe Fax: +49 721 69 40 92
76128 Karlsruhe, Germany http://wwwipd.ira.uka.de/~odersky
