The madness of implicit parameters: cured?

[Ben Rudiak-Gould]

When I first learned about implicit parameters I thought they were a great
idea. The honeymoon ended about the time I wrote some code of the form
"let ?foo = 123 in expr2", where expr2 used ?foo implicitly, and debugging
eventually unearthed the fact that ?foo's implicit value was not being set
to 123 in expr2. That was enough to scare me off of using implicit
parameters permanently.

More recently, I've realized that I really don't understand implicit
parameters at all. They seemed simple enough at first, but when I look at
an expression like

    f x = let g y = ?foo in g

I realize that I have no idea what f's type should be. Is it

    (?foo :: c) => a -> b -> c

or is it

    a -> ((?foo :: c) => b -> c)

? As far as I can tell, these are not the same type: you can distinguish
between them by partially applying f with various different values of ?foo
in the implicit environment. GHC tells me that f has the former type, but
I still have no idea why: is it because g has an implicit ?foo parameter
and f implicitly applies its own ?foo to g before returning it? Why would
it do that? Or is it because ?foo is here interpreted as referring to an
implicit parameter bound in the call of f, instead of in g? That doesn't
make sense either.

The final straw was:

    Prelude> let ?x = 1 in let g = ?x in let ?x = 2 in g
    1
    Prelude> let ?x = 1 in let g () = ?x in let ?x = 2 in g ()
    2

This is insanity. I can't possibly use a language feature which behaves in
such a non-orthogonal way.

Now the interesting part: I think I've managed to fix these problems. I'm
afraid that my solution will turn out to be just as unimplementable as my
original file I/O proposal, and that's very likely in this case since I'm
far from grokking Haskell's type system. So I'm going to present my idea
and let the gurus on this list tell me where I went wrong. Here we go.

First, discard the current implicit-parameter scheme entirely. (I'll
eventually build up to something very similar.)

Now introduce the idea of "explicit named parameters" to Haskell. This
requires three extensions: a new kind of abstraction, a new kind of
application, and a way of representing the resulting types.

The abstraction could be done with a new lambda form, but instead I'll use
a special prefix on identifiers which are to be considered named
parameters, namely the character #. The new application form will be
[F] { #x = [G] } where [F] and [G] are expressions. [F] must evaluate to a
function with an explicit named parameter #x.

The type notation for a named parameter will be (#name :: type). They can
appear only on the left side of a ->. Named parameters can only be passed
by name, so their order relative to positional parameters and each other
doesn't matter; therefore we may as well "bubble them up" to the head of
the list of arguments. In fact, we could put them in the context with the
type classes, but I won't do so.

Examples:

    cons :: (#elem :: a) -> (#list :: [a]) -> [a]
    cons #elem #list = #elem : #list

    cons { #elem = 'h', #list = "ello" }	-- legal

    cons 'h' "ello"	-- illegal: named params must be passed by name

    cons { #list = "ello" }	-- legal, has type (#elem :: Char) -> String

    cons { #list = "ello", #elem = 'h' }	-- legal

    cons { #list = "ello" } { #elem = 'h' }	-- legal

    append :: (#right :: [a]) -> [a] -> [a]
    append left #right = ...		-- named args gravitate left

Now introduce the idea of "auto-lifted named parameters". I'll distinguish
these from ordinary named parameters by using an @ prefix instead of #.
These are exactly the same as ordinary named parameters except that if
they appear in the type on the right hand side of an application node,
they are implicitly lifted to the whole node. For example, if [F] has an
auto-lifted parameter @p, and [G] has auto-lifted parameters @p and @q,
then [F][G] is implicitly converted to something like
\@p @q -> [F] { @p = @p } ( [G] { @p = @p, @q = @q } ).

Finally, introduce the following syntax:

    * As an expression, ?x is short for \@x -> @x.

    * On the left hand side of the = sign in a named application, ?x is
      the same as @x.

    * For backward compatibility, "let ?x = [E] in [F]" should be treated
      as equivalent to "[F] { ?x = [E] }".

Now we have something almost the same as the current implicit-parameter
system, except that it behaves in a much safer and saner way.

For example, looking at the confusing expressions from the beginning again:

    f x = let g y = ?foo in g

        This obviously has type (?foo :: c) -> a -> b -> c. It doesn't
        matter where the ?foo parameter appears in the type because it will
        always be referred to explicitly, by name, exactly once in each
        call of f.

    let ?x = 1 in let g = ?x in let ?x = 2 in g

        This reduces as follows:

          let ?x = 1 in let g = ?x in let ?x = 2 in g
          ( let g = \@x -> @x in g { @x = 2 } ) { @x = 1 }
          (\@x -> @x) { @x = 2 } { @x = 1 }
          2 { @x = 1 }

        At this point we get a type error, as we should: a let binding of
        an implicit parameter that's never used is almost certainly a coding
        error.

    let ?x = 1 in let g () = ?x in let ?x = 2 in g ()

        Reduces in exactly the same way as the previous case, with the
        same result. Again, this is as is should be.

Why are the semantics so much clearer? I think the fundamental problem
with the existing semantics is the presence of an implicit parameter
environment, from which values are scooped and plugged into functions at
hard-to-predict times. By substituting a notation which clearly means "I
want this implicit parameter of this function bound to this value right
now, and if you can't do it I want a static type error", we avoid this
ambiguity.

More thoughts, assuming this all pans out (knocking on wood):

  * Explicit named parameters seem like a useful idea too. Maybe they should
    be added to Haskell.

  * We should really, really drop the "let ?x" form and switch to the
    record-update notation. In "( let g = ?x in g { ?x = 2 } ) { ?x = 1 }"
    it's obvious what's going to happen and what the result will be, but in
    "let ?x = 1 in let g = ?x in let ?x = 2 in g" it's very unclear, even
    though, under the translation above, these two forms are equivalent.

  * I think it may be possible to extend this to provide default values for
    named parameters, which would be really really cool (no more separate
    foo and fooBy functions).


-- Ben