[Haskell-cafe] Limits of deduction

[Stefan Holdermans]

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