7 votes

Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?

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 ...
user avatar
  • 1,882
6 votes
Accepted

Higher-rank polymorphism over unboxed types

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. ...
user avatar
5 votes
Accepted

Universe polymorphism: the inference of universes and their constraints

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 ...
user avatar
  • 26.6k
5 votes
Accepted

Decidability of rank-k polymorphism vs. System F

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 ...
user avatar
  • 4,746
4 votes
Accepted

Commutativity of addition in polymorphic lambda calculus

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\!\!\...
user avatar
3 votes

Language/type system closest to Haskell without general recursion

The language closest to Haskell without general recursion is Haskell without general recursion, with suitable fold operations taken as primitive. Haskell's ...
user avatar
  • 26.6k
1 vote

Higher-rank polymorphism over unboxed types

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 ...
user avatar
  • 382

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