•A kind of
natural numbers
–Classifies
types Z, S Z, S (S Z)…
•These types
do not classify any runtime computations
•Lists with
length n
–List a n: list with objects of type “a” whose length
is “n”
–Equality
qualifications constrain types
•A list (Cons x xs) has the type (List a (S m)) provided that the list xs has the type (List a m)