5
$\begingroup$

To perform type inference in the presence of polymorphic recursion, one can use a Kleene-Mycroft iteration to compute the principal type of an expression. To type $\mathsf{fix}\ f\ldotp e$, we define $F(\sigma)$ as the principal type of $e$ under the assumption that $f : \sigma$. We can then define $\sigma_0 = \forall a \ldotp a$ and $\sigma_{i+1} = F(\sigma_i)$, until we reach a fixed-point $\sigma_k$. This $\sigma_k$ is then the principal type of $\mathsf{fix}\ f\ldotp e$.

There are two key issues with this:

  • Inference with polymorphic recursion is undecidable, so this iteration may not always reach a fixed-point.
  • The approximation at each stage of the iteration is not sound: if we quit after $j<k$ iterations, not only will $\sigma_j$ not be the principal type of $\mathsf{fix}\ f\ldotp e$, but it will not be a type of $\mathsf{fix}\ f\ldotp e$ at all, since we made too strong of an assumption about the type of $f$ when checking $e$.

I'm wondering if there's a standard way to soundly approximate polymorphic recursion: that is, to iterate some number of times, and afterwards, obtain a type that is possibly less general than the principal type, but that is nevertheless a valid typing of $\mathsf{fix}\ f\ldotp e$.

For example, one can imagine the Hindley-Milner approximation, where we type $e$ under the assumption that $f$ has a monomorphic type, as being the 0-ary approximation. We may fail to find a typing for an expression that requires polymorphic recursion, but if we find a type, we know that it is a valid typing of the expression.

Does such an approximation exist?

$\endgroup$
6
$\begingroup$

You should have a look at the following paper -- and the previous work by Gori and Levi:

On Polymorphic Recursion, Type Systems, and Abstract Interpretation
Marco Comini1, Ferruccio Damiani2, Samuel Vrech, 2008

The problem of typing polymorphic recursion (i.e., recursive function definitions rec {x = e} where different occurrences of x in e are used with different types) has been investigated both by people working on type systems and by people working on abstract interpretation. Recently, Gori and Levi have developed an abstract interpreter that is able to type all the ML typable recursive definitions and interesting examples of polymorphic recursion. The problem of finding a type system corresponding to their abstract interpreter was open.

In this paper we present a type system corresponding to the Gori-Levi abstract interpreter. Interestingly enough, the type system is derived from the system of simple types (which is the let-free fragment of the ML type system) by adapting a general technique for extending a decidable type system enjoying principal typings by adding a decidable rule for typing recursive definitions. The key role played in our investigation by the notion of principal typing suggests that this notion might be useful in other investigations about the relations between type systems and type inference algorithms synthesized by abstract interpretation.

$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.