Type inference for free?

Hello everybody, this is my first post, so please be gentle... (actually i was passive around here for years, and find LtU a great source of inspiration and wisdom).

I'm not at all into dynamic typing, i find static type-checking superior in any way. However, recently i just had the thourght:

"If all I want to write is a single side-effect-free, IO-free, terminating function F(x), with well defined argument- and return-types. And further, if I am able to come up with an x which trigger all branches (selections and pattern matches) of F, then i can get static (compile time) typing of F in a dynamically strong typed language."

Suppose i write F in the dynamically strong typed language, which does the following:

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.

Is this sound? If yes, what about the next step:

If it shows be the evaluation that F(x) has a strong typing, would it be possible to record all types of all expressions and create G, equivalent to F decorated with type annotations?

I do realize i'm asking for (usually turing-complete) type-infernce for free...

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

RE: Type inference for free?

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).

Would Really Like To See The Proof...

I think all of us n00bs would learn a lot from seeing the proof.

The discussion here might

The discussion here might prove instructive.

termination is irrelevant

I'm aware of the reduction to the HALTing problem, but note that I'm only interested in terminating functions, in the first place. This is a very reasonable constraint if F is a simple compiler, for example. So, if it turns out that F runs forever it is not correct and I dont really care if its type-safe.

Do you just asume that F is

Do you just asume that F is terminating, or do you mean that F should be implemented in a terminating (incomplete) language?

I assume that F is

I assume that F is terminating - that is - if I implemented it correctly. It may turn out that it is not terminating but then F is not correct, according to my own spec.

You can say, obviously, that i will never know if F is terminating on all inputs, but this is all very secondary to the question.

I'm not interested in a proving correctness, just whether it possible to make valuable analyses, like type-reconstruction.

Not sure if I am following you

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

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?

The question is underconstrained

The question is underconstrained, you need to specify more about the intended type system. E.g. I can easily think of untyped lambda terms that can be given accurate types whose subexpressions can't (in e.g. a H-M type system.)

Further if the language does not have subject reduction of whatever specified type system then there are terms that have different types than you'd get by evaluating them. More dramatically, the language clearly has to be sound w.r.t. the specified type system.

In other ways there are various ways the term could "work out" all right, but not be typeable in whatever type system.

There are cases where there is no finite set of "characteristic values" let alone a single one. Even when there is, it is (in general) impossible to be sure.

I think.....

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! :-)


Abstract Interpretation

It's not totally clear to me what you're suggesting, but I suspect that Tom Lord is right in pointing to abstract interpretation. It sounds a lot like you're suggesting a form of abstract interpretation, and on my reading (which may be way off the mark) you seem to be suggesting that you're willing to accept a possibly non-terminating abstract interpretation in order to learn more about those programs which do terminate. The relationship between types and AI has been explored here before, and I think you'll find some thought-provoking stuff in this thread (including such gems as Shan's comment "Type checking is abstract evaluation", which could really hardly fail to be relevant...)

Non-standard semantics

I think you could package up any type-inference cast as abstract interpretation as a nonstandard semantics with such a characteristic value. I'm not sure that's interesting (for Hindley-Milner, just add bags of equality constraints as "values", or something like that). Also, I'm sure any reasonable interpreter for your language doesn't actually work over that domain of values.

I thought about test driven

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.