On Tue, Jun 23, 2009 at 9:25 PM, Ross Mellgren<rmm-hask...@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 <d...@zednenem.com>
<http://www.eyrie.org/~zednenem/>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
