[Haskell-cafe] GADTs and bar :: Foo t1 -> Foo t2
dagda at xtra.co.nz
Sun Feb 19 16:06:25 EST 2006
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
data FooA = A
data FooB = B [FooA]
data FooC = C [FooB]
data Foo = FA FooA | FB FooB | FC FooC
data Node a = N [a] deriving Show
data Tree a = Zero a | Succ (Tree (Node a)) deriving Show
data EXFoo where
EXFoo :: Foo a -> EXFoo
Embarrassingly simple! :)
On Friday 17 February 2006 19:18, Daniel McAllansmith wrote:
> 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
> > 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?
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
More information about the Haskell-Cafe