On 10/6/07, Andrew Coppin
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?
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.
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... -- Dan