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?

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

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. Stuff the type system was never ever intended to do.

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!)

Type families are a step in that direction: http://haskell.org/haskellwiki/GHC/Type_families Appended is a small example of defining singleton numeral types. Manuel -=- {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE TypeOperators #-} module Numerals where data Z -- empty data type data S a -- empty data type data SNat n where -- natural numbers as singleton type Zero :: SNat Z Succ :: SNat n -> SNat (S n) zero = Zero one = Succ zero two = Succ one three = Succ two -- etc...we really would like some nicer syntax here type family (:+:) n m :: * type instance Z :+: m = m type instance (S n) :+: m = S (n :+: m) add :: SNat n -> SNat m -> SNat (n :+: m) add Zero m = m add (Succ n) m = Succ (add n m)