[Haskell-cafe] Re: Amazing
bugfact at gmail.com
Sun Feb 15 17:00:15 EST 2009
How practical is this dependent types thing? I hear a lot about this from
really clever people who are usually 10 years ahead of their time :)
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 at iro.umontreal.ca>wrote:
> > So IMO static typing is good, but it's only with functional programming
> > 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.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe