Ronald J. Legere wrote:
| quantified type must be hidden, why not just hide it at teh start?
| Can I allways do it? Is this somehow related to deMorgans law
| or something? Or is there a truly convincing example out there?
I have had the same opinion for some years, but when I recently discussed
this view with John Hughes he came up with the following example:
data Expr a = Val a | forall b . Apply (b -> a) b
(I am not sure about the syntax though, but you see what I mean). You
might imagine functions going over the structure of an Expr, counting the
number of Apply's, or calculating the value. I don't think it is possible
to "encode" this without existential types.
I have another example myself:
data Action = forall b . Act (IORef b) (b -> IO ())
If instead of IORef, there had been a functor, it would have been no
problem, we would just have mapped the function over it. But now, I can
have several different "IORef b"s shared by different "Action"s.
This is an example that came up when I was experimenting with concurrency
monads, but I found a completely different solution where I was able to do
without existentials at all (see JFP, May 1999, A Poor Man's Concurrency
Monad).
But actually, on page 318 (section 3.3), I define a run function for
this monad which has the type:
run :: C m a -> m ()
(The details are not important here, you can look into the paper if you
want, which is also on my homepage). The point is that the "m ()" really
should have been an "m a", so that you can look at the result of "C m a".
This turned out to be impossible without existential types.
A simplification of this problem comes when you encode every monad as a
continuation:
data C res m a = Cont ((a -> m res) -> m res)
Now, we can see "C res m" as a monad type, and we can embed all actions in
a monad "m" in "C res m":
lift :: m a -> C res m a
lift m = Cont (\cont -> do a <- m; cont a)
But this "res" type is floating around all the time! It is really
annoying, and it turns out to be the final result type when we are running
the monad:
run :: C res m res -> m res
run (Cont f) = f return
As you can see, we can now look at the result of the computation "C res m
res". As a result, all operations in the monad "C res m" need to be
polymorphic in "res". A really silly restriction, which could have
been avoided by local quantification.
Regards,
Koen.
--
Koen Claessen http://www.cs.chalmers.se/~koen
phone:+46-31-772 5424 e-mail:[EMAIL PROTECTED]
-----------------------------------------------------
Chalmers University of Technology, Gothenburg, Sweden
