[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