Evan Ireland writes:
> My formal proposal for existential types in Haskell is "make them the same as
> in Hope+C".
This message is to point out some of the difficulties and possible
solutions we have encountered with existential types.
It seems to be rather difficult to establish soundness of type systems
with existential types. The reason is that these systems usually rely
on "Skolemization", a meta-logical construct. In fact, the original
type system of Hope+C seems to be unsound, since Skolem-constants can
escape the body of polymorphic functions and therefore cause different
types to be identified. Here is a (simplified) example:
Suppose we have a heterogeneous list of windows:
ws:: [ex a. Win a => a]
and an indexing function
index:: [ex a. Win a => a] -> Int -> ex a. Win a.
Then,
index ws 1 :: ex a. Win a => a
index ws 2 :: ex a. Win a => a
but, since the list is heterogeneous, we can not expect that the result
of the two applications of "index" are the same. This is reflected by
the fact that (ex a. Win a => a) is a type scheme, not a type. To get
at the "true" type of a value, the value has to be "opened". In our
example, both index-applications have to be opened separately,
resulting in two different types. Therefore, all is well in type
systems such as Mitchell & Plotkin's which have true existential
types.
If we use Skolemization, however, it is easy to run into problems if we
are not careful. The "obvious" Skolemized type for index would be
[Win A => A] -> Int -> Win A
(Skolem constants written as single capitals here). But then,
index ws 1: A
index ws 2: A
and we conclude that "index" returns the same type every time!
So why not use Mitchell&Plotkin's system, which does not rely on
Skolemization? Unfortunately, this system does not have the principal
type property, and, therefore, has no type reconstruction.
A system which *has* principal types and comes with a soundness proof
is the topic of Konstantin Laufer's thesis at NYU which is currently
being written up. This system also uses Skolemization, but it
carefully restricts the scopes of Skolem constants. The problem of
designing a type system for existential types that has the principal
type property and at the same time does not rely on Skolemization
is still open, as far as I know.
Martin Odersky
Yale University
References:
@inproceedings{
AUTHOR = "Mitchell, J. and Plotkin, G.",
BOOKTITLE = "Proc. 12th ACM Symp. on Principles of Programming Languages",
PAGES = "37-51",
TITLE = "{Abstract Types have Existential Type}",
YEAR = "1985"}
@inproceedings{
AUTHOR = {K. L\"{a}ufer and M. Odersky},
TITLE = {Type Classes are Signatures of Abstract Types},
BOOKTITLE = {Proc. Phoenix Seminar and Workshop on Declarative
Programming},
MONTH = nov,
YEAR = {1991}
}
@inproceedings{
AUTHOR = {L\"{a}ufer, K. and Odersky, M.},
TITLE = {An Extension of ML with First-Class Abstract Types},
BOOKTITLE = {Proc. ACM SIGPLAN Workshop on ML and its Applications},
YEAR = {1992}
}
