All types are first class types
Closed under function type constructor
Closed under product type constructor
Closed under coproduct type constructor
Universal type is supertype of all types
Universally and existentially quantified type schemes