•Stating static
properties is a good way to think about
programming
•It may lead to more
reliable programs
•The compiler should
ensure that programs maintain the
stated properties
•Generalizing algebraic
datatypes make it all possible
–Ranges other than “T
a”
–“a” becomes an index
describing a static property of x::T
a
–New kinds let “a” have
arbitrary structure
–Computing over “a” is
sometimes necessary
–