It is not unreasonable to ask at this point why we would go through the
rigors of ordinal numbers and set theory to describe a type which we have
already defined axiomatically. Indeed, the axiomatic definition introduced
a new induction principle which superceded all prior principles, and followed
nicely from our prior work. So why consider the set theoretic approach?
This first month of the course has been a tightly-knit combination of type
theory and ``mathematical preliminaries'', which have been built hand-in-hand.
By considering the set based definition, we have shown that
this relationship remains valid even on powerful types such as inductive types.
Understanding the mathematics of inductive types helps us to further
understand the semantics of a language such as ML.
It is equally important to understand the set theoretic approach to inductive
types so that we can understand how it will later fail. While the strong
relationship between types and sets is a nice one, it can be
extended only so far. In
future lectures, we will see how the mathematical approach can become
cumbersome and insufficient as we introduce the function operator
into the
inductive types, and even more so when we consider co-inductive types.
--- End of Forwarded Message