There have been some nice papers about simple type inference for System F: "HMF: Simple Type Inference for First-Class Polymorphism", "Practical type inference for arbitrary-rank types", and "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism". These algorithms require varying amounts of annotations from the user in order to do the type inference. I am unable to find any papers on how to do type inference for System F-omega though. My questions:

  1. Can the above algorithms be extended to handle System F-omega (maybe with some more required annotations)? Or do the type lambdas require a different approach?
  2. Given that explicitly typed (Church-style) System F-omega is easy to type check, could we use one of the above algorithms to do type inference on the System F subset while requiring explicit types for the type lambdas, or do the type lambdas "infect" the other parts so that we cannot do this.
  3. Is type inference for System F-omega simpler than type inference for dependent types or do they basically need the same techniques (higher-order unification)?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.