Re: Is FPH implemented in GHC?

Am Sonntag, 14. September 2008 16:11 schrieben Sie:
| To implement all this stuff, I had to do quite a bit of code obfuscation. | That is, I introduced a lot of trivial functions only to give them an | explicit impredicative/rank 2 type signature.
But impredicative is not the same as rank-2. GHC has done higher-rank types for ages; but impredicative instantiation is a different story. Are you sure that's the bit you need? Can you give an example?
Simon
Hello Simon, I know that rank 2 is something different. I need both, rank 2 and impredicativity. I already mentioned the (impredicative) type SSignal t (forall t'. SignalFun t' a). The full type of my switch operator is SSignal t (forall t'. SignalFun t' a) -> SignalFun t a. Some of the trivial functions, I mentioned above, have rank 2 types, some have impredicative types. The latter ones typically have types of the form f (forall t. signal t a) -> f (forall t. signal' t a') where f is some specific functor. And as far as I understood, FPH brings advantages for both rank n and impredicativity. Am I wrong at this point? Best wishes, Wolfgang

| Some of the trivial functions, I mentioned above, have rank 2 types, some have | impredicative types. The latter ones typically have types of the form | | f (forall t. signal t a) -> f (forall t. signal' t a') | | where f is some specific functor. Aha -- that's impredicative all right. Good thanks. | And as far as I understood, FPH brings advantages for both rank n and | impredicativity. Am I wrong at this point? No, you're right. Simon
participants (2)
-
Simon Peyton-Jones
-
Wolfgang Jeltsch