Mark Lillibridge wrote:
>
> Claus Reinke wrote:
> > `First class modules' are just that: modules that are also first
> > class data objects of the programming language (e.g., records
> > containing functions).
>
> I would alter that to "(e.g., records containing functions _and
> types_)", at least for statically typed programming languages. I don't
> think you can justify calling something that cannot contain types, a
> module, in such languages.
Well, it's not obvious to me how the extension of a programming
language P with both types T and (first class) modules M should look
like and I'm quite sure there is more than one possible approach.
?
/ \
M T
\ /
P
Starting with an untyped language, we could first add modules, then
try to type modular programs MP (left side), or we could first add
types, then try to modularize typed programs TP (right side).
1. T T M M
M / / \ T \
\ = MP / = TP
P P
Of course, the story does not end here in either case. In the typed
modular language TMP, we want to have a modular structure for our
type language, too. In the modular typed language MTP, we still need
to make modules first class, thus giving them types.
2. M M T T
\ T \ M / /
/ = TMP \ = MTP
MP TP
The question is: how do we avoid an endless unfolding here? Are there
fixpoints, how do they look like? Do both lines have a common goal?
Your approach, influenced by the powerful SML module language, seems
to follow the right path (geometrically;-) first, then introduces one
type language covering both occurrences of T in the last right
picture (2.right). Result: first class modules with types inside!
[please correct me if I'm misinterpreting you]
The right path has an interesting intermediate alternative: using
different type systems for P and MTP does not yield first class
modules, but corresponds to the two-level design of the current SML
core and module language.
Now what about the left path? Coming from an implicitly and
dynamically typed framework, it is no surprise that I'm a little bit
biased towards this alternative, but how does it fit into the Haskell
framework (which is typed)? The reason is simple: the official module
system, representing the state-of-the-art of 1980, is just too
inflexible. It helps to organize the global namespace into smaller
environments, connected by a network of import/export-relations, and
that's it. Not even support for parameterized modules!
Without a powerful module language, Haskell programmers had to resort
to other techniques to do modular programming. Perhaps starting with
Hughes `Why functional programming matters', and continuing up to
recent publications on the construction of `modular interpreters',
Haskell's module system has received the small interest it deserves.
It's modules are not program building blocks themselves but they
contain collections of those, and the real program construction goes
on in the base language (of course, along the communication lines
allowed by import/export- declarations). So the Haskell picture
developed like this:
3. M M
\ T \ T
/ ===> /
P MP
I.e., we have a rather limited upper module language (Modula-style),
and inside there is a typed programming language whose features are
explored for (and form the main basis of) a modular programming
style. The usability of the core language constructs for such a
pupose is severely limited by the type system. Result: while extending
P with additional constructs towards a modular base language MP, the
main problems are the necessary extensions of T.
Finally, although the paths were different, the pictures 3.right and
2.left are remarkably similar, and the next natural step for Haskell
seems to be a system of first-class modules (through first-class
structures with polymorphic components) without type components to
fully establish the inner MP in 3.right, with the additional upper
module language still in place. Just as the current SML design has
two type languages, this design would have two module languages.
(Actually, there is even a third module language in the game, as the
type class system has its own means to structure type declarations..)
I agree with you that this next step would probably not be the final
word on modules (though we might have different opinions on what is
missing), but it would really be nice to see this next step taken (or
at least scheduled) in the not too distant future. Hence my question
to the Haskell committee.
It is a nice surprise to meet you here (hope you'll be up and about
again soon). By the way, do you have information about the module
language of ML2000? Will translucent sums be the basis? Is the
discussion on higher-order functors versus first-class modules
settled or still open? What were the arguments? Is there a
possibility to follow the design process? (The latest information I
have is due to Robert Harper, expressing a tendency towards keeping
the stratified language design, back in 1995.)
Does the little picture story given above make sense to you, or to
other members of this mailing list?
> @InProceedings{harper+:sharing,
> author = "Robert Harper and Mark Lillibridge",
> title = "A Type-Theoretic Approach to Higher-Order Modules with
> Sharing",
> pages = "123--137",
> booktitle = "Twenty-first {ACM} Symposium on Principles of
> Programming Languages",
> year = 1994,
> address = "Portland, OR",
> month = "January"
> }
In this paper, you mentioned that the undecidability of type-checking
for your system may not be a problem in practice. Do you have further
experience with/evidence for this conjecture?
--
Claus Reinke University of Kiel
email: [EMAIL PROTECTED] Department of Computer Science
http://www.informatik.uni-kiel.de/~cr/ Preusserstr. 1-9, 24105 Kiel
