On Tue, Jun 23, 2009 at 9:25 PM, Ross Mellgren<rmm-haskell@z.odi.ac> wrote:
I'm no expert, but it seems like those constructors should return Foobar NoZoo, unless you're nesting so there could be a Zoo, in which case the type variable a should transit, for example:
data Foobar a where Foo :: X -> Y -> Foobar NoZoo Bar :: X -> Y -> Foobar NoZoo Baz :: Foobar a -> Foobar a Zoo :: Foobar NoZoo -> Foobar Zoo
value = Zoo $ Foo (X 1) (Y 'a') value2 = Zoo $ Baz $ Foo (X 1) (Y 'a') -- value3 = Zoo $ Baz $ Zoo $ Foo (X 1) (Y 'a') -- Couldn't match expected type `NoZoo' against inferred type `Zoo' -- Expected type: Foobar NoZoo -- Inferred type: Foobar Zoo -- In the second argument of `($)', namely -- `Baz $ Zoo $ Foo (X 1) (Y 'a')' -- In the expression: Zoo $ Baz $ Zoo $ Foo (X 1) (Y 'a')
That is, if you construct a Baz with something else that doesn't have a Zoo (e.g. NoZoo) then the resultant type is also NoZoo. The converse is true.
Why would you want it to generate a polymorphic Foobar when it definitely is NoZoo?
You might have a higher-arity constructor and want to construct things like, Qux (Foo X Y) (Zoo (Bar X Y)) What's the type of Qux? If Foobar Zoo means "might contain a Zoo", then you can just declare data Foobar a where Foo :: X -> Y -> Foobar a Bar :: X -> Y -> Foobar a Zoo :: Foobar NoZoo -> Foobar Zoo Qux :: Foobar a -> Foobar a -> Foobar a and everything is fine. On the other hand, if Foobar Zoo means "definitely contains a Zoo", then you need type families to express the type of Qux. Qux :: Foobar a -> Foobar b -> Foobar (EitherZoo a b) type family EitherZoo a b :: * type instance EitherZoo Zoo Zoo = Zoo type instance EitherZoo NoZoo Zoo = Zoo type instance EitherZoo Zoo NoZoo = Zoo type instance EitherZoo NoZoo NoZoo = NoZoo -- Dave Menendez <dave@zednenem.com> <http://www.eyrie.org/~zednenem/>