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


6

I've thought a bit about this. The main issue is that in general, we don't know how big a value of polymorphic type is. If you don't have this information, you have have to get it somehow. Monomorphisation gets this information for you by specializing away the polymorphism. Boxing gets this information for you by putting everything into a representation of ...


5

It's complicated because universe constraints are simplified during inference (in order to avoid an explosion of constraints). Have a look at: Matthieu Sozeau and Nicolas Tabareau: Universe Polymorphism in Coq, Interactive Theorem Proving - 5th International Conference, ITP 2014 Beta Ziliani & Matthieu Sozeau: A Unification Algorithm for Coq featuring ...


4

The conclusion of [Kfoury & Tiuryn 1992] says (emphasis mine): We prove that [...] for every $k\ge 3$ there is a typing of constants that assigns types in $S(1)$ such that the type reconstruction problem for $\Lambda_k$ extended by this typing is undecidable. Unfortunately, this result does not give any clue as to whether type reconstruction ...


4

The fact that $\mathsf{Add}\ u\ v = \mathsf{Add}\ v\ u$ is not provable for arbitrary $u$ and $v$ does indeed follow from the Church-Rosser property. Write $u =_\beta v$ if $u \mathrel{({}_\beta\!\!\leftarrow\cup\rightarrow_\beta)^\ast} v$, where $\rightarrow_\beta$ is $\beta$-reduction in System F and $(\cdot)^\ast$ is the reflexive-transitive closure ...


3

The language closest to Haskell without general recursion is Haskell without general recursion, with suitable fold operations taken as primitive. Haskell's datatypes have non-wellfounded values thanks to Haskell's lazy evaluation strategy. Once we remove general recursion from Haskell, the difference between lazy and eager evaluation does not matter anymore,...


1

This seems to be closer to a compilation problem than a "theoretical computer science" problem, so you're probably better off asking elsewhere. In the general case, indeed, I think there is no other solution than using a boxed representation. But I also expect that in practice there are many different alternative options, depending on the specifics of your ...


Only top voted, non community-wiki answers of a minimum length are eligible