<br><br><div class="gmail_quote">On Sat, Jun 26, 2010 at 12:07 AM, Andrew Coppin <span dir="ltr"><<a href="mailto:andrewcoppin@btinternet.com">andrewcoppin@btinternet.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div class="im">wren ng thornton wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
And, as Jason said, if you're just interested in having the same programming style at both term and type levels, then you should look into dependently typed languages.<br>
</blockquote>
<br></div>
Out of curiosity, what the hell does "dependently typed" mean anyway?</blockquote><div><br></div><div>The types can depend on values. For example, have you ever notice we have families of functions in Haskell like zip, zip3, zip4, ..., and liftM, liftM2, ...?</div>
<div><br></div><div>Each of them has a type that fits into a pattern, mainly the arity increases. Now imagine if you could pass a natural number to them and have the type change based on that instead of making new versions and incrementing the name. That of course, is only the tip of the iceberg. Haskell's type system is sufficiently expressive that we can encode many instances of dependent types by doing some extra work. Even the example I just gave can be emulated. See this paper:</div>
<div><a href="http://www.brics.dk/RS/01/10/">http://www.brics.dk/RS/01/10/</a></div><div><br></div><div>Also SHE:</div><div><a href="http://personal.cis.strath.ac.uk/~conor/pub/she/">http://personal.cis.strath.ac.uk/~conor/pub/she/</a></div>
<div><br></div><div>Then there are languages like Coq and Agda that support dependent types directly. There you can return a type from a function instead of a value.</div><div><br></div><div>Jason</div><div><br></div></div>