[PRL] first-class polymorphic values

Dave Herman dherman at ccs.neu.edu
Sun Feb 25 10:50:35 EST 2007


> GHC.  Also, to plug my own work, Typed Scheme:

Cool, thanks.

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

Consider my example again, but let's imagine we could infer the return 
type of g (I'll use "?" to mean "please infer a type for this position"):

     f :: forall a . a -> (forall b . (a,b))
     fun f = \x.\y.(x,y)

     g :: forall b . [b] -> ?
     g (x:_) = f x

If the inferencer is stupid about substitution, it'll instantiate the 
type of f with b for a and infer

     forall b. (b,b)

as the return type, which is wrong. Instead it needs to freshen the 
binder and infer

     forall c. (b,c)

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

Sure. Now, even with first-class polymorphic values, there's still a 
phase separation, where all type instantiation happens at compile-time, 
right? Do you know of any languages that allow runtime type 
instantiation of polymorphic values?

Thanks again,
Dave



More information about the PRL mailing list