[Haskell-cafe] Type system trickery

[David Menendez]

On Tue, Jun 23, 2009 at 9:25 PM, Ross Mellgren<rmm-haskell at 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 at zednenem.com>
<http://www.eyrie.org/~zednenem/>