Andrew,
Right. So what you're saying is that for most program properties,
you can partition the set of all possible problems into the set for
which X is true, the set for which X is false, and a final set for
programs where we can't actually determine the truth of X. Is that
about right?
Yes, you can. (Although, as far as I know, one typically partitions
into (a) the set for which is true (respectively false) and (b) the
union of the set for which X is false (true) and the set for which we
cannot determine X. But, of course, being able to do so implies that
you can apply the partitioning that you suggest.)
I find it interesting that one quite hard looking property - "this
program is well-typed" - can always be deduced. Perhaps that's
because the language is specifically designed to constrain the set
of possible programs in such a way that this is possible? Or
perhaps it's just that the set of programs which can't be proved
well-typed are simply rejected as if they were provel ill-typed?
*shrugs*
That's exactly it. A prototypical example is the Haskell program
(if True then 2 else 'x') + 3
Of course, this is a type-safe program in the sense that it will
never actually result in adding a character and a number; but still,
for a large class of statically typed languages, such a program will
be rejected.
Cheers,
Stefan
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
