[Haskell-cafe] Type-level arithmetic

[Andrew Coppin]

Dan Piponi wrote:
> 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?
>   

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