Hi Fergus!
> Can anyone explain to me what "first class structures" are,
> and how they differ from (or relate to) existential types?
Probably many things are called `first class structures', but I guess
that you mean Mark Jones' first class structures -- that is, the work
in his paper ``From Hindley-Milner Types to First-Class Structures''
and his recent POPL paper. If that is not what you mean, you can hit
the <delete> key of your mail reader now.
In my understanding, a first class structure is roughly a collection
of *polymorphic* functions that you can pass around as a value. The
important point is that these functions are actually polymorphic and
not just *instances* of polymorphic functions. 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'
allows to pull the universal quantification of `a' inside the data
structure. (The curly braces indicate a structure type, which consists
of a list of type assertions. Regard it as a record with a field for
every type assertion.)
So if we define
idstruct :: Id
idstruct = struct -- this builds a structure
id x = x
we can use it as in
let
mystruct = idstruct
in
(mystruct.id 1, mystruct.id "bla")
This gives no type error! Each time we access the function named `id'
that is stored in `mystruct', we may instantiate its type anew. In
contrast, something like
let
nostruct = let id x = x in AId id
in
(case nostruct of
AId f -> f 1,
case nostruct of
AId g -> g "bla")
gives a type error. (Defining `id' globally with a polymorphic type
wouldn't help, as its use in building `nostruct' requires the
commitment to a concrete instance.)
Now to your questions about the comparison with existential types. As
I understand it, it is essentially the difference between existential
and universal quantification. It has the following implications for
the types where such a data structures is constructed and decomposed.
Construction.
- Universal quantification (first class structures): This is an
occurrence of the keyword `struct', where functions are defined,
which (like any polymorphic function) may not make any assumptions
about the types of the universally quantified variables.
- Existential quantification: We can put any type in place of an
existentially quantified one (but we have to commit to one) --
although, the information about the type that we have chosen is
lost.
Decomposition.
- Universal quantification: This is access to a structure component
using the `dot notation'. The universally quantified type
variables can be instantiated to any type (operationally that is
justified, because the function definition did not make any
assumptions about the type).
- Existential quantification: No assumption may be made about the
existentially quantified type (in the type system, we get a skolem
constant here, any constraint on such a constant leads to a type
error).
So, you see that both systems are in some sense opposites. Both must
not make any assumption in one position and may take any concrete type
in the other position. But the positions are exchanged in both
systems.
I hope that this was not too confusing (and I hope even more that Mark
can agree on this explanation :-)
Cheers,
Manuel
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
Manuel M.T. Chakravarty, Technical University Berlin, IKS, Germany
Virtual home: http://www.cs.tu-berlin.de/~chak/
[EMAIL PROTECTED], IRC: Chilli
