[Haskell-cafe] Type-level arithmetic

[Dan Piponi]

On 10/6/07, Andrew Coppin <andrewcoppin at btinternet.com> 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?

> 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