[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Generalizing Types as Provable Invariants
Matthias Felleisen <firstname.lastname@example.org> 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
> 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
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)