Home

FPH: First-class Polymorphism for Haskell

FPH: First-class Polymorphism for Haskell, by Dimitrios Vytiniotis, Stephanie Weirich and Simon Peyton Jones:

Languages supporting polymorphism typically have ad-hoc restrictions on where polymorphic types may occur. Supporting “firstclass” polymorphism, by lifting those restrictions, is obviously desirable, but it is hard to achieve this without sacrificing type inference. We present a new type system for higher-rank and impredicative polymorphism that improves on earlier proposals: it is an extension of Damas-Milner; it relies only on System F types; it has a simple, declarative specification; it is robust to program transformations; and it enjoys a complete and decidable type inference algorithm.

Under Related Work, the authors provide a detailed comparison of their system with MLF, and HMF.

By naasking at 2008-04-20 16:46 | Functional | Type Theory | other blogs | 9067 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

No discussion of FCP

I'm surprised the authors don't discuss Mark Jones' work on FCP (cf. First-class polymorphism); it certainly seems to qualify as "annotation-driven type inference for first-class polymorphism". I'm guessing they want to talk about annotations directly to System F terms, and so don't count use of inductive types to mark places that need quantifiers.

Edited: fix last word.

By Charles Stewart at Mon, 2008-04-21 08:55 | login or register to post comments

I could be mistaken, but

I could be mistaken, but doesn't this stick to predicativity?

By Philippa Cowderoy at Mon, 2008-04-21 12:21 | login or register to post comments

Theorem 4

I understand theorem 4 of MPJ's paper to be asserting an embedding of System F in FCP.

By Charles Stewart at Mon, 2008-04-21 12:54 | login or register to post comments

Polymorphism guarded by constructors

It seems to be that the system from that paper only allows polymorphic values guarded inside constructors. Section 6.1 seems to be explaining how to define a new data type for each polymorphic type in the System F program. Many languages have at least that much support for polymorphic values now.

The other systems mentioned here allow first class polymorphism without defining data types, just with lambdas and hopefully few annotations. MLF at least actually extends the type language so you don't have to commit to a type scheme for functions like the identity which can be used at incomparable (in System F) types, id :: (forall a . a -> a) -> (forall a . a -> a) or id :: forall a . ((a -> a) -> (a -> a)).

By Brandon Moore at Wed, 2008-05-07 12:36 | login or register to post comments