> type inferencer

> compile time type checking

Aren't those the same thing?

No. A type inference does not check types. It inferences types.

For example if you know that + is defined for numbers, then you can inference that a and b must be numbers: (+ a b)

If you know that a and b are numbers then you can inference that subexpressions need to deal with numbers only:

   (let ((a c) (b d)) (declare (type number a b)) ....)

The type inferencer then will tell what types the various expressions have. It will try to propagate known types as widely as possible in the code.

Allegro CL and LispWorks for example are doing this type inference. But their compiler will not tell you that type declarations are violated.

SBCL OTOH treats type declarations as type assertions which can be checked at compile time. ADDITIONALLY it also does type inference - and additionally uses this information for compile time type checks.

> A type inference does not check types. It inferences types.

OK, on that definition, of what possible use is a type inferencer? Aren't they useful only as a component of a compile-time type checker?

Convenience.

Basically CCL's compiled code is often as fast as code from SBCL, LispWorks, Allegro CL. But one has to declare much more types of variables and functions explicitly with CCL. The code needs to be littered with type declarations.

A compiler with a (better) type inferencer can propagate the type information it already has and this is often enough for fast code. A good compiler can then also tell the developer where it lacks type information and then you can decide to declare types explicitly. SBCL/CMUCL does that in a very noisy way with lots of information generated by the compiler. ;-)

See for example: http://home.pipeline.com/~hbaker1/TInference.html

Performance. If you have (+ x y) and you can infer that x and y are fixints, then you can use a couple inline opcodes, rather than calling GENERIC-+.

EDIT: lispm is right, too, of course. You can look at it either way. If your program required top performance and you were going to tag every type until it ran super fast, then inference buys you the convenience of not needing to do as much. If you weren't going to bother with that, then inference buys you extra performance without all the effort.

('Infer' is a perfectly good verb; you don't have to make one out of 'inference'. But sometimes it's easy to disremembrance things like that on HN.)

I believe lispm is not a native English speaker. His website TLD is .de.

Yes, I see. Doesn't mean he or she might not rather be correct, however.

True that.

Thanks, didn't remember that.

It's an easy mistake to make. Incidentally, "infer", for some reason, is a word I find unusually pleasing.

EDIT: as a non-native speaker I distinctly remember first reading the word and happily using it ever since, when appropriate.

And a similar possibly wrong usage is "conference" when used as a verb, maybe, since "confer" is probably okay. But "conference" seems to have become accepted, I've heard it a bit. There's this trend (from many years, not just recent) to make nouns into verbs too, e.g. "Skype me". The "confer" form as a verb probably sounds archaic to many, since it's not commonly heard or read (AFAIK).

Perfectly fair — I'm sure you're not the first to inference something. And yes, 'infer' is an interesting word, especially when you bring in Latin.

> SBCL OTOH treats type declarations as type assertions which can be checked at compile time.

Wait, is that really not the standard behavior?

CMUCL invented that in the mid/end 80s. CMUCL forks like SBCL and Scieneer CL got it there. The other compilers don't do that.

I don't think so. A type inferencer figures out types of expressions that don't have a type explicitly declared using information it has about other things that are declared.

A compile time type checker is expected to signal errors at compile time for programs whose types don't check out.

You can use a type inferencer without signaling any errors at compile time (for example, by deferring errors to runtime) and you can signal type errors at compile time even if you don't infer any types (like C compilers, that demand all variables have a declared type).