The madness of implicit parameters: cured?

[Ben Rudiak-Gould]

On Mon, 4 Aug 2003, Ashley Yakeley wrote:

> ((\a -> ((a,\@x -> @x) {@x = 2})) (\@x -> @x),\@x -> @x) {@x = 1}
                                     ^^^
> ((\@x -> @x,\@x -> @x) {@x = 2},\@x -> @x) {@x = 1}

This reduction is incorrect. The underlined parameter needs to be lifted
out, so

	(\a -> ((a,\@x -> @x) {@x = 2})) (\@x -> @x)

becomes

	\@x -> ((\a -> ((a,\@x -> @x) {@x = 2})) @x)

If we next apply (\a -> ...) to @x, something interesting happens: we
have to rename to avoid variable capture. I didn't realize this was ever
necessary with implicit parameters. The renaming is impossible with my
punning notation, so I'll have to write this out again with separate
interface and implementation names (yuck):

	\{@x=s} -> ((\a -> ((a,\{@x=t} -> t) {@x = 2})) s)

Now names of the form @x only appear on the left hand side of {...=...}
forms, as they should, and I chose different internal names for lexically
distinct bindings. Further reduction should yield the expected answer.

The key point is that /everything/ in my proposal is lexically scoped.
That's why everything works as expected. The current system uses
quasi-dynamic scoping, which is why things work pretty much as expected
most of the time but not always.

Whenever you're in doubt about the correct way to do a reduction in my
system, do whatever preserves hygiene. And the rules for lifting implicit
parameters are isomorphic to the type-inference rules for the implicit
parameter context, so if you're ever in doubt about which parameters to
lift, figure out how the type is inferred.


> A simpler query: what types can f have here? Which if any should the 
> compiler infer?
> 
>   f a b = (a,b) {@x = 2}

Yow. The compiler certainly won't infer anything for this, but if we allow
explicit typings we get stuff like

    f1 :: (Num a, Num b) => a -> ((?x :: b) => b) -> (a,b)
    f1 a b = (a,b) {@x = 2}

    f2 :: (Num a, Num b) => ((?x :: a) => a) -> b -> (a,b)
    f2 a b = (a,b) {@x = 2}

    f1 ?x ?x {@x = 1}		==> (1,2)
    f2 ?x ?x {@x = 1}		==> (2,1)

This issue never occurred to me. I'd like to just ban these types, but
they look potentially useful, and in fact I see that you use them in
HScheme. I think it's up to the community to decide this one. It's sad to
lose the nice property of independence of type, but my proposal is still a
lot better than what we've got.

Note that we also have:

    f0 :: (Num a, Num b) => a -> b -> (a,b)
    f0 a b = (a,b) {@x = 2}	==> type error: (a,b) has no parameter @x

    f3 :: (Num a, Num b) => ((?x :: a) => a) -> ((?x :: b) => b) -> (a,b)
    f3 a b = (a,b) {@x = 2}

    f3 ?x ?x {@x = 1}		==> type error: (f3 ?x ?x) has no param. @x


> And given that type, which of these are valid?
> 
>   f ?x ?x
>   f ?x 1
>   f 1 ?x
>   f 1 1

I don't think there's any way to forbid any of these while also allowing
types like those of f1 and f2 above. In fact, I don't think you can forbid
them without also forbidding

    fromJust' :: (?default :: a) => Maybe a -> a
    fromJust' (Just x) = x
    fromJust' Nothing  = ?default

I see what you're driving at, though: can/should I forbid the compiler
from inferring a type for (a,b) {@x = 2} under these circumstances? I
think the answer is "yes," but I'm not sure. Can anyone weigh in who's
actually implemented a type inferencer for Haskell?


-- Ben