
15 Sep
2008
15 Sep
'08
8:05 a.m.
| 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