RFC: Syntax for implicit parameter bindings

[John Hughes]

[Resent with permission of author -=chak]

I'm beginning to find implicit parameters *extremely* useful, so I think it's
important to get this right. I have some code that will have to change, but not
as much as I will have in a couple of years...!

I find adding a keyword to implicit parameter declarations, as in

	    let dynamic ?base = 10 in addBase 5

	  or

	    let nonrec ?base = 10 in addBase 5

just plain ugly. The question mark already indicates that this is an implicit
parameter binding, there is no need for another keyword to say the same
thing. This would make sense to me if implicit parameter names were lexically
the same as other identifiers -- but THAT would be a big mistake! Without
wanting to stir up language wars, this idea reminds me of ML rather than
Haskell. One of the great strengths of Haskell's syntax, in my opinion, is
just that it is so concise. Let's keep it that way!

I am against

	    let ?base := 10 in addBase 5

also -- not because := is already a constructor, but because I have another
proposal for how to use it! From time to time I argue for a "monomorphic
binding" operator, a substitute for the monomorphism restriction, which has
become even more necessary with the addition of implicit parameters. (See my
"Global Variables in Haskell" paper for a discussion and example). I'd like to
reserve := for monomorphic binding.

That leaves plain let bindings -- and in that case, why not also where, case,
do, and lambda?

	There was also a mention of extending the implicit parameter
	story to work as recursive bindings, but I don't know any
	details here.  It would certainly strengthen the case for
	using plain `let'.

Why not recursive bindings? Why not mix implicitly bound variables and
explicitly bound ones in the same pattern? This is surely the most orthogonal
and powerful mechanism.

The question is whether such bindings always have a clear meaning. I claim
they do. For each implicitly bound variable ?x, let's assume that x is a fresh
variable. Let e be an expression in the scope of ?x. Then I claim that
replacing each such e by 

	  e with ?x = x

and replacing the binding occurrence of ?x by x gives a sensible meaning to
the extended language.

For example,

    let ?fac n = if n==0 then 1 else n*fac? (n-1) in e

means

    let fac n = if n==0 then 1 else n*fac? (n-1) with fac? = fac
    in e with fac? = fac

And

    (\?x -> e)

means

    (\x -> e with ?x = x)

The only funny thing is that, because of the way implicit parameters are
passed, their types cannot be generalised.

John