16 Nov
2010
16 Nov
'10
3:40 p.m.
On Nov 16, 2010, at 12:36 PM, Ling Yang wrote:
Are only 'trivial' results possible, or that the incomputability problems are just moved into type space?
That's typically the case, under Rice's theorem. A construct is derivable if it works for all cases (i.e., it's a "free theorem"), or if it works for none. If it works for some, you need to encode the differences between the cases yourself.