Implicit Parameters

[Koen Claessen]

Hi all,

Now we are talking about implicit parameters, let us take up
the following problem with them on the Haskell mailing list
too.

Suppose I have the following function definition:

  app :: (?ys :: [a]) => [a] -> [a]
  app xs =
    case ?ys of
      []      -> xs
      (y:ys') -> y : (app xs with ?ys = ys')

This function appends its argument to its implicit argument,
by recursively changing the implicit argument. For example:

  Hugs> app [1,2] with ?ys = [3,4]
  [3,4,1,2]

So far so good! Now, since Haskell has type inference, we
can leave out the type signature:

  -- app :: (?ys :: [a]) => [a] -> [a]
  app xs =
    case ?ys of
      []      -> xs
      (y:ys') -> y : (app xs with ?ys = ys')

Let us check if it still works again:

  Hugs> app [1,2] with ?ys = [3,4]
  [3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,3,{Interrupted!}

And, stunningly, it doesn't! Why doesn't this work?

That is because type inference assumes that the body of
`app' is monomorphic, i.e. has no context in its type.
Therefore, the recursive call to app where ?ys is changed,
had no effect at all.

It works with the type signature there, because in order to
implement type checking (note: not type inference) with
polymorphic recursion demands to use the stated type in
checking the body of the function.

Mark Shields, Simon Peyton-Jones, and I, and also Jörgen
Gustavsson have been discussing several modest solutions to
this (we believe it is not needed to do full type inference
that can deal with polymorphic recursion to solve this
problem).

My questiona are: Were the designers of the implicit
parameters paper aware of this problem when they wrote the
paper? If so, they probably did not think this was a big
problem. Do people in general think this is a problem?

/Koen.

--
Koen Claessen
http://www.cs.chalmers.se/~koen
Chalmers University, Gothenburg, Sweden.