# Polar type inference with intersection types and ω

## Abstract

We present a type system featuring intersection types and omega, a type constant which is assigned to unused terms. We exploit and extend the technology of expansion variables from the recently developed System I, with which we believe our system shares many interesting properties, such as strong normalization, principal typings, and compositional analysis. Our presentation emphasizes a polarity discipline and shows its benefits. We syntactically distinguish positive and negative types, and give them different interpretations. We take the point of view that the interpretation of a type is intrinsic to it, and should not change implicitly when it appears at the opposite polarity. Our system is the result of a process which started with an extension of Trevor Jim's Polar Type System.

## Bibtex (lrde.bib)

@InProceedings{	  carlier.02.itrs,
author	= {S\'ebastien Carlier},
title		= {Polar type inference with intersection types and $\omega$},
booktitle	= {Proceedings of the 2nd Workshop on Intersection Types and
Related Systems (ITRS), published in: Electronic Notes in
Theoretical Computer Science},
volume	= 70,
issue		= 1,
publisher	= {Elsevier},
year		= 2002,
month		= jul,
abstract	= {We present a type system featuring intersection types and
omega, a type constant which is assigned to unused terms.
We exploit and extend the technology of expansion variables
from the recently developed System I, with which we believe
our system shares many interesting properties, such as
strong normalization, principal typings, and compositional
analysis. Our presentation emphasizes a polarity discipline
and shows its benefits. We syntactically distinguish
positive and negative types, and give them different
interpretations. We take the point of view that the
interpretation of a type is intrinsic to it, and should not
change implicitly when it appears at the opposite polarity.
Our system is the result of a process which started with an
extension of Trevor Jim's Polar Type System.}
}