X is a relatively new, untyped calculus, invented to give a
Curry-Howard correspondence with Classical Implicative
Sequent Calculus. It is already known to provide a very expressive
language; embeddings have been defined of the lambda-calculus,
Bloo and Rose's lambda-x, Parigot's lambda-mu and Curien and Herbelin's lambda-bar-mu-mu-tilde.
We investigate various notions of polymorphism in the
context of the X-calculus. In particular, we
examine the first class polymorphism of System F, and the shallow
polymorphism of ML. We define analogous systems based on the
X-calculus, and show that these are suitable for embedding the
original calculi.
In the case of shallow polymorphism we obtain a more general
calculus than ML. A type-assignment algorithm is
defined for this system, which generalises Milner's W.
