Laws, type constructors, kinds and higher-order polymorphism.