The madness of implicit parameters: cured?

[Ashley Yakeley]

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

>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.

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})

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}


-- 
Ashley Yakeley, Seattle WA