The madness of implicit parameters: cured?

[Ben Rudiak-Gould]

On Mon, 4 Aug 2003, Ashley Yakeley wrote:

> At 2003-08-04 20:00, Ben Rudiak-Gould wrote:
> 
> >This is a different lambda calculus, with a different beta rule. You can
> >see the same effect in the type inference rules for implicit parameters:
> >If f has type Int -> String and ?x has type (?x :: Int) => Int, then f ?x
> >has type (?x :: Int) => String, i.e. the implicit ?x parameter is lifted
> >out of the RHS to become a parameter of the whole application node. This
> >rule is what makes implicit parameters implicit.
> 
> Ah. Actually I think the beta rule is unchanged with Haskell's implicit 
> parameters. Consider:
> 
>   x :: (?x :: Int) => Int
>   f :: Int -> String
>   f :: ((?x :: Int) => Int) -> ((?x :: Int) => String) -- specialisation
>   f x :: (?x :: Int) => String -- apply beta rule

I think it amounts to the same thing. This is a nice way of looking at it,
though. Either way, the effect is that implicit parameters don't
"disappear" into function applications unless the function has been
explicitly typed to take them; instead they grow to encompass larger and
larger portions of the containing function, until eventually they become
parameters of the whole function. Result: you don't have to put them there
by hand.

> So is this valid or not?
> 
>   b :: (?x :: Int) => Int
>   b = \@x -> @x
> 
>   f :: ((?x :: Int) => Int) -> (Int,Int)
>   f = \a -> ((a,\@x -> @x) {@x = 2})
> 
>   f b :: (Int,Int)
>   f b = ((b,\@x -> @x) {@x = 2})
>    = ((\@x -> @x,\@x -> @x) {@x = 2})

Yes, it is. This illustrates what you pointed out earlier, that the
program's semantics can be changed by adding explicit type signatures
which include implicitly-parameterized parameters.

> If it is valid, then this must be a valid reduction:
> 
>   ((\a -> ((a,\@x -> @x) {@x = 2})) (\@x -> @x),\@x -> @x) {@x = 1}
>   ((\@x -> @x,\@x -> @x) {@x = 2},\@x -> @x) {@x = 1}

Not unless you give an explicit type signature, no. Without it the
compiler will infer a different type for f which does not have any
arguments with implicit parameters, because inferred types never do (see
section 2.1 in the original paper). Without this assumption the compiler
couldn't infer a principal type. (Specialization doesn't help here,
because the set of valid specializations depends on f's internals, and
can't be captured by a principal type.)


-- Ben