[PRL] first-class polymorphic values
Sam TH
samth at ccs.neu.edu
Sun Feb 25 09:42:07 EST 2007
On 2/25/07, Dave Herman <dherman at ccs.neu.edu> wrote:
> I know that FX supported first-class polymorphic values, and O'Toole and
> Gifford have a PLDI'89 paper on supporting type inference in languages
> with polymorphic values. Does anyone know of other languages that have
> allowed first-class polymorphic values?
GHC. Also, to plug my own work, Typed Scheme:
(pdefine: (a) (f [x : a]) : a x)
(define: (g [y : (All (a) (a -> a))]) : Boolean
(y 3)
(y #t))
(g f)
> Do type checkers for higher-rank polymorphism have to consider type
> equality up to alpha-equivalence of type names?
Yes - or at least, I did.
> Do inference algorithms
> for languages with higher-rank polymorphic types have to freshen type
> names when they synthesize polymorphic types?
I don't see why they would. When you infer the type for:
f x = x
you can infer ALL a. a -> a without needing to have a fresh a, since
we're synthesizing the binder too. But I haven't done this myself.
> One last question: is there a distinction between "first class
> polymorphic values" and "higher-rank polymorphism"?
Well, "higher-rank" can mean multiple things. We wouldn't consider a
language that allowed functions with type
((N -> N) -> N) but not (((N -> N) -> N) -> N)
to have "first class" functions, I don't think. So I don't think
rank-2 polymorphism would count as "first class". But arbitrary rank?
I think so.
--
sam th
samth at ccs.neu.edu
More information about the PRL
mailing list