Talk:Type arithmetic

Why?

This page seems to explain what but not why. I don't know about anyone else, but when I read 'arithmetic at the type level', the very first thought that pops into my head is 'why in the name of God would you want to do such an insane thing?' MathematicalOrchid 11:53, 12 March 2007 (UTC)

This why?

Following some discussions in #haskell, I understand this is related to that widespread Haskell obsession with attempting to "prove" things about programs (in spite of the fact that this is obviously impossible).

If I'm understanding this right, the idea is to be able to construct a type that means not merely "a List containing Integers", but "a List containing at least 6 Integers". And the "arithmetic" part comes in when one wants to say something like

"This function takes a List containing at least X objects of type T and another List containing at least Y objects of type T, and returns a List containing at least X+Y objects of type T."

In other words, the "arithmetic" part is calculating X+Y at compile-time. And any function that calls the one so-described must prove to the type system that it satisfies the constrains. And, once the constraints are statically verified, no further runtime checks are required.

Is that roughly what this is all about? (And if so, can somebody add some statements to that effect to the content page?) MathematicalOrchid 20:07, 12 March 2007 (UTC)

One example

I'm working on code where I need to handle a stack of objects of different types. I like the security of type-safety, so I use HList instead of creating a universal wrapper type, wrapping all the elements, and using a homogenous list. But to index into a heterogenous list, you have to use a type-level index. Then to be able to manipulate the indices, you need to be able to do type-level arithmetic.

Not necessarily something you'd do every day, but when it's needed, it's needed. --Nedervold 04:26, 14 March 2007 (UTC)