(This is a message on strictness, etc. I was too busy to reply
earlier when the discussion first began).
Like Ian, I would like to suggest that we lift functions in Haskell.
Originally there was a good reason not to: there was no need (and
indeed no way) to distinguish _|_ from \x->_|_. But now there are
some compelling reasons to make the distinction:
1) It solves the strict constructor business without resorting,
for example, to Simon's "Data" class.
2) This in turn solves the lifted/unlifted product and ADT issue
without resorting to a new kind to datatype decl ("newtype").
3) It makes theory closer to practice: Haskell will look more like
Abramsky and Ong's lazy lambda calculus.
4) It conforms better to (at least my) intuition: current Haskell
implementations in a sense CAN distinguish _|_ from \x->_|_:
just return a functional value from the whole program, and in
one case the implementation is likely to print something like
"function", and in the other case, nothing (or "error", or whatever).
To formalize this we could include a bulit-in instance decl for
functions in the class Text.
Ian proposes to use subtypes to capture strictness. This may be a
reasonable suggestion, but a lot more work needs to be done to
understand the ramifications; certainly looking at recent work on
strictness analysis via type inference is a starting point for exploring
this idea (maybe the type system SHOULD enforce the strictness
annotations!).
Alternatively, we could just have a pre-defined function "strict"
(ala Stoy, for example), that when applied to a function, returns
its strict version. Its type would be (a->b)->(a->b) (the same
as that of "apply"), although an argument could be made for making
it a method (along with, perhaps, "apply") in a class called
"Applicable", or "Function", or whatever.
Then with no other extensions, strict can be used to make any function
or constructor f strict in its nth argument by writing
strict (f x1 ... xn-1). Of course, we'd probably want some syntax to
make this easier, especially to allow pattern matching. For example:
1) for constructors, use ! annotations in data decls, as in LML.
2) for functions, use ! annotations in type sigs (which then looks
like Ian's suggestion, but not in terms of subtypes). For example,
it's then trivial to define seq:
seq :: !a -> b -> b
seq x y = y
In any case, I think it helps to think of all this in terms of "strict".
What are the disadvantages of having strict constructors?
I think the main one is that we lose some degree of equational
reasoning, as Warren points out. On the other hand, this problem
already exists to a degree; for example to make a datatype truly
abstract I won't even reveal that it's a constructor, by renaming
it as a function; this causes the same problem that Warren mentioned.
What are the disadvantages of having a lifted function space?
I think the main one is that we lose unrestricted eta conversion.
But maybe that's not such a big deal either.
-Paul
---
Professor Paul Hudak
Department of Computer Science
Yale University
P.O. Box 208285
New Haven, CT 06520-8285
(203) 432-4715
[EMAIL PROTECTED]
