The Pinafore type system is based on Stephen Dolan's Algebraic Subtyping, an extension of HindleyMilner to allow subtyping. You can see his POPL talk here. Pinafore omits recursive types and record types.
Familiarity with HindleyMilner is assumed.
Positive and Negative Types
Dolan typing distinguishes positive and negative types.
Roughly, a positive type is the type of a value, while a negative type is the type of accepting a value.
Subtyping relations are of the form A <= B
, where A
is a positive type and B
is a negative type.
You can read A <= B
to mean "every A is a B", or that something of type A
will be accepted as a B
.
This relation is of course reflexive and transitive.
For example, if P > Q
is a positive type, then P
is a negative type, and Q
is a positive type.
Given a function f : P > Q
and a value a : T
, then the application f a : Q
is allowed if T <= P
.
(Alternatively, if P > Q
is a negative type, then P
is a positive type, and Q
is a negative type.)
Covariance and Contravariance
More generally, every type parameter of a type is either covariant or contravariant. Covariant parameters have the same polarity (positive or negative) as the type they are in, while contravariant parameters have the opposite.
If T
has a covariant parameter,
A <= B
implies T A <= T B
If T
has a contravariant parameter,
A <= B
implies T B <= T A
Intuitively, the word "of" suggests covariance, while the words "for" and "on" suggest contravariance.
For example, a number is a literal (Number <= Literal
), and a list of numbers is a list of literals ([Number] <= [Literal]
).
Thus "list of" is covariant.
And an order on literals is an order on numbers (Order Literal <= Order Number
).
Thus "order on" is contravariant.
Any & None
Any
and None
are the top and bottom of the type hierachy. That is, for any P
, we have None <= P
and P <= Any
.
Any
is only a negative type, and None
is only a positive type.
Conjunction and Disjunction
If P
and Q
are positive types, then P  Q
is a positive type.
This represents "untagged union", that is, the type of values that may be P
or may be Q
, but there is no way of determining which.
If P
and Q
are negative types, then P & Q
is a negative type.
A value passed to a P & Q
must be both a P
and a Q
.
Type Variables
As in Haskell, the first letter is upper case for type constants, and lower case for type variables.
Type variables play essentially the same role as they do in HindleyMilner typing, though in the context of Dolan typing they are best understood as connecting (negative) inputs to (positive) outputs. Type variables on only one side can be eliminated.
Type Simplification

Any type variables that appears only in the positive position are replaced by
None
. Likewise, any only in the negative position, withAny
.
\x y > x : a > b > a
→\x y > x : a > Any > a
[] : [a]
→[] : [None]

None
andAny
act as identities for
and&
, respectively.
Int  None
→Int

Redundant types in joins (

or&
) are eliminated.
Text & Text
→Text
.
More generally, ifP <= Q
then
P  Q
→Q
P & Q
→P

Matching parameterised types are collapsed along their parameters. For example:
(A > X)  (B > Y)
→(A & B) > (X  Y)
[A] & [B]
→[A & B]

Type variables are merged if they appear in all the same positive positions, or in all the same negative positions.
a > b > (a  b)
→a > a > a
(a
andb
appear in the same set of positive positions)
Type Ranges
To represent a parameterised type with a parameter that would not ordinarily be either covariant or contravariant, a type range is used.
This is simply a pair of type parameters, one contravariant (indicated with a minus sign) and one covariant (a plus sign).
Type ranges in types are typically represented by the form {p,+q}
, where p
is the contravariant parameter and q
the covariant.
However, the syntax permits any number of commaseparated items. For example, in positive position:
T {}
= T {Any,+None}
T {+a}
= T {Any,+a}
T {+Int,a,Entity}
= T {(a & Entity),+Int}
In negative position,
T {}
= T {None,+Any}
T {+a}
= T {None,+a}
T {+Int,a,Entity}
= T {(a  Entity),+Int}
And also,
T A
= T {A}
= T {A,+A}
T +A
= T {+A}
T A
= T {A}
It's important to remember that 
and +
indicate contravariance and covariance, not negative and positive polarity.