GADTs and bar :: Foo t1 -> Foo t2

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

GADTs and bar :: Foo t1 -> Foo t2

Daniel McAllansmith
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@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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: 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@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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe