Yes, that web page is a terrible introduction to dependent types. :)<br><br><div><span class="gmail_quote">On 10/6/07, <b class="gmail_sendername">Andrew Coppin</b> <<a href="mailto:andrewcoppin@btinternet.com">andrewcoppin@btinternet.com
</a>> wrote:</span><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">Dan Piponi wrote:<br>> On 10/6/07, Andrew Coppin <<a href="mailto:andrewcoppin@btinternet.com">
andrewcoppin@btinternet.com</a>> wrote:<br>><br>>> I've seen quite a few people do crazy things to abuse the Haskell type<br>>> system in order to perform arithmetic in types.<br>>><br>><br>
> How did you know precisely what I was doing at this moment in time?<br>><br><br>Birthday paradox?<br><br>>> Stuff the type system<br>>> was never ever intended to do.<br>>><br>><br>> There's "didn't intended that it be possible to" and there's "intend
<br>> that it be impossible to". Hmmm...maybe one of these should be called<br>> cointend.<br>><br><br>Ouch. You're making my head hurt...<br><br>>> Well I was just wondering... did anybody ever sit down and come up with
<br>>> a type system that *is* designed for this kind of thing? What would that<br>>> look like? (I'm guessing rather complex!)<br>>><br>><br>> Well there are always languages with dependent type systems which
<br>> allow you to have the type depend on a value. In such a language it's<br>> easier to make types that correspond to some mathematical<br>> constructions, like a separate type for each n-dimensional vector.
<br>> (See <a href="http://www.haskell.org/haskellwiki/Dependent_type.">http://www.haskell.org/haskellwiki/Dependent_type.</a>) But that's<br>> kind of cheating. I'm guessing you're talking about a language that
<br>> makes it easier to "fake" your own dependent types without properly<br>> implementing dependent types. If you find one, I could use it right<br>> now - the details of embedding the gaussian integers in Haskell types
<br>> are getting a bit complicated right now...<br>><br><br>...I have no idea what you just said.<br><br>(The wiki article is pretty special though. An entire raft of dense<br>equations with no attempt to provide any background or describe what any
<br>of this gibberish *is*. Clearly it made sense to the author, but...)<br><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">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br></blockquote></div><br>