Monotype

type-theory

Definition

Monotype

A monotype is a type with no explicit universal quantifier.

In a simple function-type grammar, monotypes are generated by

$$\tau ::=\alpha \mid b\mid {\tau }_1\to {\tau }_2,$$

where $\alpha$ is a type variable, $b$ is a base type, and ${\tau }_1\to {\tau }_2$ is a function type.