[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