Jeff,
> Isn't that a bit of a dodgy argument? I don't know of any papers on `in'
> polymorphism, but many about `let' polymorphism. If I see `let', I expect
> polymorphism, and I'm not going to go searching for an `in'.
Not true (or if true, misguided). Consider the type rule for "let". The
generalization only takes place in the context for the body of the "let" (the bit
after the "in"), and not in the context of the declarations themselves. This is
why extra work is needed to achieve polymorphic recursion, that is, where "let"
declarations are indeed polymorphic in their own scope. In the absence of an
explicit type annotation the use would be monomorphic. In the absence of let
restructuring, the same would apply to any other uses of the variable (function)
in the same binding group.
> It's been proposed before that we have a separate notation for monomorphic
> bindings. I'd like to see you adopt this approach, rather than having `let'
> in `do' behave fundamentally differently. This example also provides nice
> example and motivation for introducing a monomorphic let notation.
This could make sense if done throughout the language. Our proposal is intended
to be much more modest.
> The ability to bind multiple things at once (and have the corresponding
> increase in polymorphism) is a nice feature of a modern `let' - but it's not
> the primary characteristic. The let in do could easily bind multiple things
> as well (by allowing `in'). The currently syntax is just an aesthetic choice
> isn't it?
The current "let" in "do" already can bind multiple things. The reason for omitting
the "in" is explicitly to avoid introducing another scope level (requiring a new "do",
a new indent, etc.). How one expects it to behave depends on the implicit
assumptions made about all the variables being bound in the "do". Currently,
even though "do" gives the appearance of introducing many variables all at the same
declaration level, it actually intoduces a nested sequence of variable bindings,
each possibly shadowing bindings earlier in the sequence. In this current setting
it makes sense for "let" in "do" to be thought of having an implicit "in", and so
its bound variable is polymorphic in the remainder of the "do". In a recursive "do"
(as in a "let"), all the newly bound variables are actually considered to be in
a concurrent scope -- as suggested by the layout. In this setting, any variables bound
by "let" are also part of the same scope as the others -- we have one big binding
group -- hence they are monomorphic when used by other declarations in the same
binding group.
John.
