Re: What's wrong with C++?

["Peter C. Chapin" <PChapin@vtc.vsc.edu>]

On Thu, 17 Feb 2011, Dmitry A. Kazakov wrote:

>> Could you elaborate a little on why you think type inference is bad? In 
>> the functional languages that support it, type inference is completely 
>> type safe (for example: Haskell, OCaml, Scala). Perhaps you mean 
>> something different.
>
> The first notice is that inferred types cannot be safe per definition.
> There is no additional information involved. What is inferred, already is.
> To me safety is when some a-priori information unknown to the compiler (and
> to the language designers) is used to detect sematic problems.

I understand this point. I believe you are saying that types are part of the 
program's design and thus asserting them in the program explicitly (and 
having the compiler check the resulting code) brings information from the 
design into the compiler's view.

> The second note is that if types are not the things from the problem space 
> (of which the compiler knows little or nothing), then what kind of stuff 
> is there in their place? I presume that nothing.

You can still define the types you need. Inference just means that you 
typically don't have to bother with explicit declarations: create the 
objects you need (of the types you need) and let the compiler work out the 
details.

> Now the main objection is computability and decidability. Only "simple" 
> things can be inferred. The compiler cannot solve problems beyond 
> Turing-completeness...

It sounds like you are taking "type inference" to mean that the compiler 
figures out pre-conditions, post-conditions, etc. I'm just talking about the 
compiler recovering type information based on how entities are used. For 
example, in OCaml:

let rec sum_items alist =
   match alist with
      [] -> 0
    | head::tail -> head + (sum_items tail)

The compiler infers that sum_items is a function taking a list of ints and 
returning an int. It does this by looking at what the code does: mylist is 
being matched against a list pattern. The head element of the list is an int 
because of its use with +. The branches of the match both agree in their 
type (int) which is the type returned by the function which is consistent 
with its use in the summation operation.

The algorithms for doing this are well understood and they are decidable. On 
the other hand there are undecidable type systems, it's true. I've heard it 
said that Scala's type system is undecidable. However, nobody much cares 
because the programs that force the type checker into nontermination are so 
weird that no normal developer would ever write them (so it is claimed).

Peter