[Haskell-cafe] Impredicativity confusion
Dimitrios Vytiniotis
dimitriv at cis.upenn.edu
Wed Aug 22 10:31:59 EDT 2007
Hi,
>
> type B = forall a. a->a
>
> boom = foo f (id :: B)
> where f = undefined :: Foo B
Unfortunately the current implementation of impredicativity
has similar problems, which can be summarized as: who gives information
(and who should give if any) in application nodes about instantiations
of variables; the arguments (and which one?) ? the result types? none?
<perhaps-confusing-explanation-skip-if-you-want>
Now the source of the particular confusion is that although "Foo B" says
that a should be instantiated with "B", the current way applications
are checked does not know how to use this information because it is
inside a "box". The point is that a "boxy" variable for "a" is filled in
(correctly) with B, but then when we are checking:
(id :: B) : this_boxy_variable
we fail because it is not the case that:
forall a. a -> a <= BOX{ forall a. a -> a}
Now, there was a good reason for that, boxes represented inferred
information that we have no idea *when* they are filled and by who.
There are more useful cases for example where we really want:
forall a. a -> a <= BOX{ tau -> tau } for any tau.
and that is what GHC chooses, and that's what happens algorithmically.
</perhaps-confusing-explanation>
The whole story of impredicativity in GHC is unsatisfactory; for now you
can circumvent your problem by simply providing yourself the correct
instantiation of foo:
boom = (foo :: Foo B -> B -> Bool) f (id :: B)
So, until something is done to fix these issues (I am thinking about it
and there exist several related reasearch proposals) a general rule for
the current implementation is: give the instantiations yourself if it
fails to check.
I hope this helps more than confuses,
-dimitris
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
More information about the Haskell-Cafe
mailing list