| And what can
we do about this? How can we obtain a programming language from a system
where only very few functions are expressible? Well, there are two different
choices. The first one is to move to a more complex type discipline. And
this is something we will see in a moment in this same lecture. The other
choice, which is the one followed by Standard ML, is to add a typed constant
to the languages. So, let's add to the language a constant fix (or Y) that
computes the fixed point of a function. If we have a function M from A to
A, fix (M) computes an element of A which is a fixed point for M. It is
clear from this very definition that fix allows the definition, the computation
of arbitrary recursive functions. Therefore, from the typed l-calculus and fix we get again a typed calculus where all Turing computable functions are expressible. This, as I said, is the choice of Standard ML. But for other purposes, for the purpose of proof checking or for the purpose of having logical frameworks, it is quite handy to have more complex, more expressive typed disciplines. | 
|
