Re: I/O
Evan Ireland says As Nigel and I have pointed out to numerous people (including Haskell committee members), the statement that stream I/O cannot be efficiently emulated by continuation I/O is true only if the continuation model being used is lacking in certain request types (i.e. references/assignment as in Tui or coroutines as in Hope+C). I thought Paul Hudak's seminal paper 'On the Expressiveness of Purely Functional I/O Systems' had shown that stream I/O was COMPLETELY equivalent to continuation I/O. Or is the emphasis above to be taken to be on the word 'efficiently'? I didn't see the discussion leading up to this. It would be interesting to see stuff about existential types. It doesn't appear to have been on the haskell mail system. Tony Davie
Objects with state, or FP + OOP = Haskell++
John, My formal proposal for existential types in Haskell is "make them the same as in Hope+C". If you do not have a copy of Nigel Perry's PhD thesis, I can ask Nigel to send you one (I am having some bound copies made now). Also I seriously suggest that the Haskell committee look at continuation-style I/O as a primitive, and dispense with the stream model altogether. Keeping an underlying stream model is sure to hold back developments in functional language I/O (at least with Haskell), such as manipulating objects with state, having polymorphic requests, and introducing concurrency. As Nigel and I have pointed out to numerous people (including Haskell committee members), the statement that stream I/O cannot be efficiently emulated by continuation I/O is true only if the continuation model being used is lacking in certain request types (i.e. references/assignment as in Tui or coroutines as in Hope+C). Stream I/O is only useful for making stupid programming mistakes. I am sure the I/O semantics can be easily defined without it. Lets improve the I/O for Haskell 2. Committee members and Haskell implementors: please make some comment on these proposals (with justification if you don't want to junk the stream model). ___ [EMAIL PROTECTED] Evan Ireland, Department of Computer Science, +64-6-3569099 x8541 Massey University, Palmerston North, New Zealand.
Re: I/O
| Tonny Davie says | | Evan Ireland says | | As Nigel and I have | pointed out to numerous people (including Haskell committee members), the | statement that stream I/O cannot be efficiently emulated by continuation I/O i | true only if the continuation model being used is lacking in certain request | types (i.e. references/assignment as in Tui or coroutines as in Hope+C). | | I thought Paul Hudak's seminal paper 'On the Expressiveness of Purely Functional | I/O Systems' had shown that stream I/O was COMPLETELY equivalent to continuation | I/O. Or is the emphasis above to be taken to be on the word 'efficiently'? Regarding efficiency, can someone comment on whether there is any difference between the stream and continuation models in the effect on parallelism? --Joe
Objects with state, or FP + OOP = Haskell++
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 MitchellPlotkin'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}
}
