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

Daniel McAllansmith dagda at xtra.co.nz
Fri Feb 17 01:18:11 EST 2006


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


More information about the Haskell-Cafe mailing list