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)
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
