The madness of implicit parameters: cured?

[Ben Rudiak-Gould]

On Mon, 4 Aug 2003, Ashley Yakeley wrote:

> At 2003-08-04 18:19, Ben Rudiak-Gould 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.
> 
> It's a simple beta-reduction, it must be correct.

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.

As you pointed out, this reduction behavior depends on f's type, so this
is necessarily a typed lambda calculus. But that's okay because Haskell is
statically typed.


-- Ben