Re: [Haskell-cafe] Type-level arithmetic

Yes, that web page is a terrible introduction to dependent types. :) On 10/6/07, Andrew Coppin wrote:

Dan Piponi wrote:

...

On 10/6/07, Andrew Coppin wrote:

...

I've seen quite a few people do crazy things to abuse the Haskell type system in order to perform arithmetic in types.

How did you know precisely what I was doing at this moment in time?

Birthday paradox?

...

...

Stuff the type system was never ever intended to do.

There's "didn't intended that it be possible to" and there's "intend that it be impossible to". Hmmm...maybe one of these should be called cointend.

Ouch. You're making my head hurt...

...

...

Well I was just wondering... did anybody ever sit down and come up with a type system that *is* designed for this kind of thing? What would that look like? (I'm guessing rather complex!)

Well there are always languages with dependent type systems which allow you to have the type depend on a value. In such a language it's easier to make types that correspond to some mathematical constructions, like a separate type for each n-dimensional vector. (See http://www.haskell.org/haskellwiki/Dependent_type.) But that's kind of cheating. I'm guessing you're talking about a language that makes it easier to "fake" your own dependent types without properly implementing dependent types. If you find one, I could use it right now - the details of embedding the gaussian integers in Haskell types are getting a bit complicated right now...

...I have no idea what you just said.

(The wiki article is pretty special though. An entire raft of dense equations with no attempt to provide any background or describe what any of this gibberish *is*. Clearly it made sense to the author, but...)

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe