[TYPES] Decidable intersection-type inference for general recursion: state of the art?

[Stefan Holdermans]

Hi all,

This is a question about principal typings and decidable type inference for general recursion in the context of type systems like System I, System E, ... .

In [KW04] and [KWW02] type inference for recursive definitions is left as future work and marked as challenging as it interferes with the polar nature of the inference algorithm. Also, the work on System E does not seem to make any mention of general recursion.

Can anyone tell me what is today's state of the art with respect to principality and (rank-restricted) intersection-type inference for recursive definitions?

Thanks,

  Stefan


[KW04] A.J. Kfoury and J.B. Wells: Principality and type inference for intersection types using expansion variables. Theor. Comput. Sci. 311(1-3): 1-70 (2004)

[KWW02] A.J. Kfoury, G. Washburn, J.B. Wells: Implementing compositional analysis using intersection types with expansion variables. Electr. Notes Theor. Comput. Sci. 70(1): 124-148 (2002)