[Haskell-cafe] Re: Amazing

[Peter Verswyvelen]

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
> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090215/953c47a1/attachment.htm