oleg@pobox.com wrote: ] ] One way is to use existentials: ]
data Seq1 a = forall b. (Pre a b, Show b) => Cons1 a (Seq1 b) | Nil1
] ] which perhaps not entirely satisfactory because we have to specify all ] the needed classes in the definition of Seq1. Yes, that seems pretty burdensome, since we can't now create even a simple function like "tail", right? Or at least I think existentials are the problem with this...
tail1 :: (Pre a b, Show b) => Seq1 a -> Seq1 b -- tail1 (Cons1 x xs) = xs tail1 Nil1 = error "empty Seq"
...ghci reports... Couldn't match expected type `b' (a rigid variable) against inferred type `b1' (a rigid variable) `b' is bound by the type signature for `tail_' at dec2.lhs:30:17 `b1' is bound by the pattern for `Cons1' at dec2.lhs:31:8-17 Expected type: Seq1 b Inferred type: Seq1 b1 In the expression: xs In the definition of `tail1': tail1 (Cons1 x xs) = xs ...and hugs... ERROR "dec2.lhs":31 - Existentially quantified variable in inferred type *** Variable : _3 *** From pattern : Cons1 x xs *** Result type : Seq1 _0 -> Seq1 _3 ] ] 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. <snip> ] > data Cons a b = Cons a b ] > data Nil = Nil ...if we build our lists with tuple-like Conses, our types end up being as long as our lists, right? So an infinite list has an infinite type, which seems like it could be problematic to type check. For example, here's an arbitrarly long increasing list...
data Seq' a = Cons' a (Seq' (Succ a)) | Nil' deriving Show
from :: a -> Seq' a from x = Cons' x (from (S x))
inf = from Z
...with some of the usual functions...
tail_ :: Seq' a -> Seq' (Succ a) tail_ (Cons' x xs) = xs
class Take a where take_ :: a -> (Seq' b) -> (Seq' b)
instance Take Zero where take_ Z _ = Nil'
instance Take a => Take (Succ a) where take_ (S n) (Cons' x xs) = Cons' x (take_ n xs) take_ _ Nil' = error "can't take_ that many"
class Drop a b c | a b -> c where drop_ :: a -> Seq' b -> Seq' c
instance Drop Zero b b where drop_ Z xs = xs
instance Drop a (Succ b) c => Drop (Succ a) b c where drop_ (S n) (Cons' x xs) = drop_ n xs drop_ _ Nil' = error "can't drop_ that many"
...Anyway, for fun, here's a list that alternates between two types in a linearly increasing manner. So you can start out with one Int and then two Strings, then three Ints, four Strings, etc. I don't know if it is going to yeild to a type classless GADT solution yet, but I'll keep thinking about it.
data Fancy a b left next = forall c d left' next' lz decleft . (Show c, Show d, Zerop left lz, If lz (Succ next) next next', Pre left decleft, If lz next decleft left', If lz b a c, If lz a b d ) => Cons a (Fancy c d left' next') | Nil
fancy :: Fancy Integer String Zero (Succ Zero) fancy = (Cons 1 (Cons "a" (Cons "b" (Cons 2 (Cons 3 (Cons 4 (Cons "c" (Cons "d" (Cons "e" (Cons "f" (Cons 5 (Cons 6 (Cons 7 (Cons 8 (Cons 9 Nil)))))))))))))))
instance (Show a, Show b) => Show (Fancy a b c d) where show (Cons x xs) = "(Cons " ++ (show x) ++ " " ++ (show xs) ++ ")" show Nil = "Nil"
data Succ a = S a deriving Show data Zero = Z deriving Show
data TTrue data TFalse
class Pre a b | a -> b instance Pre (Succ a) a instance Pre Zero Zero
class If p t e result | p t e -> result instance If TTrue a b a instance If TFalse a b b
class Zerop a b | a -> b instance Zerop Zero TTrue instance Zerop (Succ a) TFalse