Greg Buchholz wrote:
I'm wondering about creating a data structure that has the type of decreasing numbers. I can try...
class Pre a b | a -> b instance Pre (Succ a) a instance Pre Zero Zero
data (Pre a b) => Seq a = Cons a (Seq b) | Nil
decreasing = Cons three (Cons two (Cons one Nil))
...but that complains about "Not in scope: type variable `b'"
One way is to use existentials:
data Seq1 a = forall b. (Pre a b, Show b) => Cons1 a (Seq1 b) | Nil1
decreasing1 = Cons1 three (Cons1 two (Cons1 one Nil1))
which perhaps not entirely satisfactory because we have to specify all the needed classes in the definition of Seq1. Perhaps a better -- and a more general alternative -- is to use type-level programming to its fullest. The following defines a list whose elements are constrained to be in the decreasing, increasing, or any other (defined in the future) order. This example shows that Haskell truly has more kinds than it is commonly acknowledged. For more details on constrained lists (list of odd numerals, even numerals, etc), please see the following implementation of Tim Sheard's `Half' example http://pobox.com/~oleg/ftp/Haskell/Half.hs
data Succ a = S a data Zero = Z
zero = Z one = S zero two = S one three = S two
class KIND l a b
data Cons a b = Cons a b data Nil = Nil
data Increasing = Increasing instance KIND Increasing a (Succ a) data Decreasing = Decreasing instance KIND Decreasing (Succ a) a -- one can add non-increasing, non-decreasing, etc.
class ConstrainedL c l instance ConstrainedL c Nil instance ConstrainedL c (Cons a Nil) instance (KIND c a b, ConstrainedL c (Cons b l)) => ConstrainedL c (Cons a (Cons b l))
-- smart constructors. -- Alternatively, define as_increasing :: ConstrainedL Increasing l => l -> l consi :: ConstrainedL Increasing (Cons a l) => a -> l -> Cons a l consi = Cons
consd :: ConstrainedL Decreasing (Cons a l) => a -> l -> Cons a l consd = Cons
incr = consi one (consi two (consi three Nil)) -- No instance for (KIND Increasing (Succ Zero) (Succ (Succ (Succ Zero)))) -- incr1 = consi one (consi three Nil)
decr = consd three (consd two (consd one Nil))
-- No instance for (KIND Decreasing (Succ (Succ Zero)) (Succ (Succ (Succ Zero)) -- decr1 = consd three (consd two (consd three Nil))