Lambda the Ultimate

Immediatly after each compile of F, evaluate F(x), (yes, please). If it does not crash (or loop forever) F is type-safe, else report an error. The idea is that type-checking F is no harder than evaluating it on a sufficiently large test set argument.

But this is precisely the problem. Your solution reduces to HALT, which isn't solvable. I think you probably are familiar with HALT and its ramifications and just overlooked this fact; but if not, I (or someone else most likely) can point you to a proof and prove that your solution reduces to HALT (it's actually quite trivial).

In the untyped lambda calculus programs don't crash anyway, so you don't need to worry about that.

However, if you only allow pure. terminating programs, you can have the simply typed lambda calculus already (Curry style; as you said you wanted type inference). You don't need to run functions against inputs. You'll know their types after typechecking.

In Research Papers section you'll see Barendregt's Introduction to Lambda Calculus. It explains these matters very clearly. Afterwards, take a look at our Getting Started thread.

Thanks for the replies.

Im not thinking of infering types of lambda calculus (this is well understood anyway) but rather contrary, of some obscure dynamical language in which no formal analysis apply.

In other words: Even though evaluation is the only tool at hand (because the language is too bizarre to be analysed in any way) it seems that I can get away with type analyses on a (well defined, not trivial) restricted set of programs (like compilers) anyway?

I'm nearly as amateurish as the top poster here but, humility aside:

I think you are excited because you have observed that static type checking is a special case of abstract evaluation and then, on top of that, you speculate that within the domain of a program we can locate a "characteristic value" whose evaluation as input parameter, by that program, has essentially the same effect as the abstract evaluation that corresponds to static type checking.

The answer, in the reformulation as a conjunction of two questions ("is type checking abstract evaluation?" and "is there a guaranteed characteristic value?") is yes/no.

Speculatively: if you limit yourself to non-complete languages, you might usefully be able to make that equivocation (but it's a long shot).

The key thing there is that what you are after is only going to be found in a non-complete language. If you glom around on LtU you can find at least some discussion of the possibility that non-complete languages are all we need but.... I wouldn't yet bank on it for any major sum... Fun to think about, though.

The other key thing is that you are reaching towards paraphrasing stuff that's already pretty well established. (Which means you should be good for at least 10 years of academic publications! :-)

-t

I thought about test driven type reconstruction myself and I always stumbled about the meaning of a type checker / abstract interpretation in that context. Most severely a change of the program code can't be responded by just letting a type checker run because the change may be valid according to the dynamically typed program but rejected by the ad-hoc generated type checker.

The most meaningfull use case for test driven type reconstruction is very likely x-compilation. Here you have a predefined type system of a target language and a type checker for it. At each instant of test driven development you might factor your code into translatable and intranslatable parts no matter how well the types got reconstructed. So you have to work out the type recorder which might be simple but also the factorization function which is quite specific.

My suggestion: less blogging and more coding :)

Thank you everyone, for commenting.
I realize that i have been overly optimistic about the 'characteristic value'. I will definitly look more into abstract interpretation as well as the threads pointed to.
Thanks.