On Fri, Feb 04, 2005 at 10:29:53AM +0100, Thomas Fischbacher wrote:

[...]
> If I multiply a speed (in m/s) with a mass (in kg),
> I get a momentum (in kg m/s), which I neither can sensibly add to a 
> speed, or a mass. If I further consider a change in momentum with time, I 
> automatically get something with units kg m/s^2, that is, a force.
> 
> Of course, I could introduce types for all intermediate quantities which I 
> will encounter in a problem statically. However, there are many problems 
> where I do not know a priori which quantities will appear with which 
> powers, hence I would like to have this with full dynamical flexibility. 

So, you have to decide, what you want: Flexibility or not?
If you want clearly typed values, you can use a language
that supports it. If not, use a language that ignores types.

But as you said above: Yes, it's necessary to have distinct types that
doesn't match and are clearly distinct and incompatible to
avoid problems where mixing up different types would be a problem.

In your example: "a momentum (in kg m/s), which I neither can sensibly
 add to a speed, or a mass."

So strictly checking types is really helpful here.

In OCaml you can use the module system to be helpful here (abstract data types).
It is possible to define incompatible types, which are also can be restricted
by value and to raise exceptions from within that types.
And because of functors it's also possible to use the same structure
but by using signatures it can be done that the types are differing.

There is an example on this in the Ocaml-book from O'Reilley.
Look for subsection "Hiding Type Implementations" in section
"Modules and Information Hiding" in Chapter 14 ("Programming with Modules").


The type system of OCaml has helped me a lot in even smaller
programs to avoid problems that would be there, when using
languages like C, where the "type system" is very loosely,
would have caused many problems. Especially when using pointer-stuff,
many Segfaults may would have appeared in the program run
(and hopefully in the testing phase), where the type system has
stopped me.

How much more helpful will it be in larger/large projects!

I didn't believe that the type system really supports the programmer
until I have worked a while with it, and especially (as mentioned
by others here), when changing code that is older (and where you
may have forgotten a lot of the program's structure because it's too
long ago, when you touched the code the last time).

In the beginning I similar to you thought: "Well, people say it might
help, and so it might help... but I really find it annoying!".
Now I see: Well, it might be annoying, when you are new to it, but
I now can see *through experience* that it DOES help in programming.
Even in small programs it is helpful!


Ciao,
   Oliver