[PRL] first-class polymorphic values

Sam TH samth at ccs.neu.edu
Sun Feb 25 11:43:22 EST 2007


On 2/25/07, Dave Herman <dherman at ccs.neu.edu> wrote:

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

This seems right.  However, I don't know of any languages that allow
type signatures like the one you gave.  They were proposed for
Haskell' here:

http://www.haskell.org/pipermail/haskell-prime/2006-January/000001.html

but they don't seem to have gotten very far, or to have considered the
issues you raise.

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

Are there any languages that keep the polymorphism around at runtime
at all?  Of the languages with "first class polymorphic functions"
(FX, GHC, Typed Scheme so far) all of them erase types before runtime.

-- 
sam th
samth at ccs.neu.edu



More information about the PRL mailing list