[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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)
