[Haskell-cafe] GADTs and bar :: Foo t1 -> Foo t2

[Daniel McAllansmith]

My thanks for the responses received off-list.

Dimitrios pointed out that a 'successor' class solution would require the 
typechecking to depend somehow on whether the lists were empty or not.
Probably a clue that I was on the wrong track.

Both Cale and Dimitrios suggested better solutions involving different data 
types:

data FooA = A
data FooB = B [FooA]
data FooC = C [FooB]
data Foo = FA FooA | FB FooB | FC FooC

or

data Node a = N [a] deriving Show
data Tree a = Zero a | Succ (Tree (Node a)) deriving Show

or

data EXFoo where
  EXFoo :: Foo a -> EXFoo


Embarrassingly simple! :)

Thanks
Daniel


On Friday 17 February 2006 19:18, Daniel McAllansmith wrote:
> Hello,
>
> I have a recursive type
>
> > data Foo = A | B [Foo] | C [Foo]
>
> that I would like to restrict so that a C can only contain Bs, and a B can
> only contain As.
> If I use a GADT as follows the bar function, understandably, will not type
> check.
>
> > data AType
> > data BType
> > data CType
> >
> > data Foo a where
> >     A :: Foo AType
> >     B :: [Foo AType] -> Foo BType
> >     C :: [Foo BType] -> Foo CType
> >
> > --get the successor of the Foo
> > bar c@(C []   ) = c
> > bar   (C (b:_)) = b
> > bar b@(B []   ) = b
> > bar   (B (a:_)) = a
> > bar a at A         = a
>
> How do I achieve this restriction?  Do I need to have some sort of
> successor class with dependent types?
>
> Ta
> Daniel
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe