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)