•Data is a parameterized generalized-algebraic datatype
•It is indexed by some semantic property
•New Kinds introduce new types that are used as indexes
•Programs use types to maintain semantic properties
•The equality constrained types make it possible