> 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?
A difference between structures and records or algebraic types is that
in the construction of a structure value you *define* a function for
each field; while in building a record or data term you put a value in
each component, which (as a special case) may just be the *use* of a
previously defined function as a value. While in a functional language,
due to functions-as-first-class-objects this may seem very similar, it
is conceptually different and carries different implications for the
type system.
In the definition of a (named) function, you generalize the types,
i.e., you universally quantify all free variables (without
constraints). But in the use of a function name (here `use' is not
necessarily application, but just mentioning the name of the function
in an expression), you instantiate the universally quantified type
variables.
The construction of a structure requires a generalization step (to get
the universal quantification). So, it corresponds to function
definition, not use. If you use a notation, such as the second-order
lambda calculus, that makes type abstraction and instantiation
explicit you can maybe handle structures by records. But as long as
you rely on this implicit assumption about generalization in
definitions and instantiation in uses, you will (as far as I see) have
to use some special syntax.
Manuel
