Re: Generalizing Types as Provable Invariants

[Pixel <address@hidden>]

Matthias Felleisen <matthias@ccs.neu.edu> writes:

> > various examples of static checks:
> > - const'ness (C++)
> > 
> > extended type systems
> > - dependent types (cf recent thread on comp.lang.functional)

i meant to add that C++ has a form of dependent types

[...]

> Pixel, if a language isn't safe, a type system is only half as helpful. 
> Think of C++. If it verifies x is a char, then at run-time it may still
> throw in some bits from an int into x, and what do you know -- is it
> an int then? No, but it will print as one. 

except from builtin-types where Bjarne Stroustrup gave up strictifying
it (whereas subtyping between number types works nicely in Java),
C++ type system is _quite_ ok.

C++ has things that allow really powerful computation on types (using
templates). The const'ness available in C++ is also quite innovative.

Now my griefs on C++ are:
- memory unsafeness
- high compilation-time (esp. with g++ + templates)
- errors messages not readable
- and hard to debug (eg: inspecting STL data structures)
- reference/pointer duality, heap/stack duality
- templates type checked when used
- explicit typing

I know C++ type system has many holes, but I don't think that's the
main problem!
 
> Is adding more stuff to such type systems truly useful? Be more selective. 

That's up to you. Choosing complexity or not is debatable (cf Python
thread)

What I meant is that C++ do have

- powerful types via templates
  (with limitations, esp. templates are invariant (subtyping))

- const'ness subtyping which other languages do not have
 
  (talking about this, i've just posted this on haskell mailing list
   (was apropos purity annotation):

  > On the subject of const'ness, I've been messing around with it.
  > I've been quite surprised to discover that Java&C# do not have C++'s
  > const (Java has "final" on parameters, but it is dumb)
  > 
  > About this: http://merd.net/inoutness.html 
  > (beware, half of it is still investigations)
  )