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

<p><a href="https://users.dimi.uniud.it/~marco.comini/Papers/PolRecTySysAbsInt/PolRecTySysAbsInt08.pdf" rel="nofollow noreferrer">On Polymorphic Recursion, Type Systems, and Abstract Interpretation</a><br>
Marco Comini, Ferruccio Damiani, Samuel Vrech, 2008   </p>

<blockquote>
  <p>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.</p>
  
  <p>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.</p>
</blockquote>

CC BY-SA 4.0
2019-07-25T13:26:49.090Z
2020-03-28T01:19:56.937Z
2020-03-28T01:19:56.937Z
gasche
<p>To perform type inference in the presence of polymorphic recursion, one can use a <em>Kleene-Mycroft</em> iteration to compute the principal type of an expression. To type <span class="math-container">$\mathsf{fix}\ f\ldotp e$</span>, we define <span class="math-container">$F(\sigma)$</span> as the principal type of <span class="math-container">$e$</span> under the assumption that <span class="math-container">$f : \sigma$</span>. We can then define <span class="math-container">$\sigma_0 = \forall a \ldotp a$</span> and <span class="math-container">$\sigma_{i+1} = F(\sigma_i)$</span>, until we reach a fixed-point <span class="math-container">$\sigma_k$</span>. This <span class="math-container">$\sigma_k$</span> is then the principal type of <span class="math-container">$\mathsf{fix}\ f\ldotp e$</span>.</p>

<p>There are two key issues with this:</p>

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

<p>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 <span class="math-container">$\mathsf{fix}\ f\ldotp e$</span>.</p>

<p>For example, one can imagine the Hindley-Milner approximation, where we type <span class="math-container">$e$</span> under the assumption that <span class="math-container">$f$</span> 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.</p>

<p>Does such an approximation exist? </p>

<pl.programming-languages><type-theory><type-inference><recursion><polymorphism>
Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?
Joey Eremondi
# Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?

(Asked by: username_0 on 2019-07-24)

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 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?

**Tags:** pl.programming-languages, type-theory, type-inference, recursion, polymorphism


---

## 1 answers

### Answer by username_1 on 2019-07-25. Score: 7

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](https://users.dimi.uniud.it/~marco.comini/Papers/PolRecTySysAbsInt/PolRecTySysAbsInt08.pdf)  
Marco Comini, Ferruccio Damiani, 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.


---

