[Haskell-cafe] Type-level arithmetic

[Manuel M T Chakravarty]

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)