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 :)<div><div><div><div><br></div><div>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 ;-).</div>
<div><br></div><div>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 ;-)</div>
<div><br></div><div>Of course back then I was even more naive than I am now, so those things are easier said than done I guess. </div><div><br></div><div>But if I understand it correctly, dependent types are a bit like that, values and types can inter-operate somehow?</div>
<div><br></div><div><div class="gmail_quote">On Sun, Feb 15, 2009 at 9:40 PM, Stefan Monnier <span dir="ltr"><<a href="mailto:monnier@iro.umontreal.ca">monnier@iro.umontreal.ca</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="Ih2E3d">> So IMO static typing is good, but it's only with functional programming that<br>
> it really shines.<br>
<br>
</div>You can go one step further: if you start using dependent types, you'll<br>
see that it gets yet harder to get your program to type-check, and once<br>
it does, you don't even bother to run it since it's so blindingly<br>
obvious that it's correct.<br>
<font color="#888888"><br>
<br>
Stefan<br>
</font><div><div></div><div class="Wj3C7c"><br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br></div></div></div></div>