Search code examples
haskelltypestype-systemstype-level-computation

Numeric type signature

Is it possible to create a type with a numeric argument?

i.e. if I want to create a type of integers with a fixed bit-width:

newtype FixedWidth w = FixedWidth Integer

addFixedWidth :: FixedWidth w -> FixedWidth w -> FixedWidth (w+1)
mulFixedWidth :: FixedWidth w -> FixedWidth w -> FixedWidth (2*w)

So that the type-checker only allows FixedWidths of the same type to be added or multiplied, but also determines the correct precision of the result.

I know you can do something like this:

data Nil = Nil
data Succ x = Succ

addFixedWidth :: FixedWidth w -> FixedWidth w -> FixedWidth (Succ w)

and represent the number 4 as Succ (Succ (Succ (Succ Nil)))), but that's incredibly ugly. I also need to figure out how to append two Succs for the multiply result type.

Solution

  • The feature you are looking for is type-level naturals, know as the -XTypeNats extension to Haskell.

    At the moment this is possibly only in an experimental branch of GHC. It is likely to merge into GHC by 7.4 I think.

    Some further reading: