[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