[Haskell-cafe] Impredicativity confusion

Dimitrios Vytiniotis dimitriv at cis.upenn.edu
Wed Aug 22 10:31:59 EDT 2007


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


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.

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,

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