Actually, back in the eighties when I was an assembly language hacker, I didn't want to switch to Pascal or C since I found the types in those languages too weak. C++ changed that with templates, and then I switched (only to find out that no C++ compiler existed that would not crash on my fully templated programs ;-).

What I really wanted was a way to program the type checks myself; verify constraints/assertions at compile time, and if the constraint or assertion could not be done at compile time, get a warning or an error (or bottom if the custom type checking program is stuck in an endless loop ;-)

Of course back then I was even more naive than I am now, so those things are easier said than done I guess.

But if I understand it correctly, dependent types are a bit like that, values and types can inter-operate somehow?

On Sun, Feb 15, 2009 at 9:40 PM, Stefan Monnier <monnier@iro.umontreal.ca> wrote:

> So IMO static typing is good, but it's only with functional programming that
> it really shines.

You can go one step further: if you start using dependent types, you'll
see that it gets yet harder to get your program to type-check, and once
it does, you don't even bother to run it since it's so blindingly
obvious that it's correct.

Stefan

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe