Injective type families?

[Conal Elliott]

Yes, it's one things that data families do. Another is introducing *new*
data types rather than reusing existing ones. - Conal

On Mon, Feb 14, 2011 at 1:41 PM, John Meacham <john at repetae.net> wrote:

> Isn't this what data families (as opposed to type families) do?
>
>    John
>
> On Mon, Feb 14, 2011 at 1:28 PM, Conal Elliott <conal at conal.net> wrote:
> > Is there a way to declare a type family to be injective?
> >
> > I have
> >
> >> data Z
> >> data S n
> >
> >> type family n :+: m
> >> type instance Z   :+: m = m
> >> type instance S n :+: m = S (n :+: m)
> >
> > My intent is that (:+:) really is injective in each argument (holding the
> > other as fixed), but I don't know how to persuade GHC, leading to some
> > compilation errors like the following:
> >
> >     Couldn't match expected type `m :+: n'
> >            against inferred type `m :+: n1'
> >       NB: `:+:' is a type function, and may not be injective
> >
> > I realize that someone could add more type instances for (:+:), breaking
> > injectivity.
> >
> > Come to think of it, I don't know how GHC could even figure out that the
> two
> > instances above do not overlap on the right-hand sides.
> >
> > Since this example is fairly common, I wonder: does anyone have a trick
> for
> > avoiding the injectivity issue?
> >
> > Thanks,  - Conal
> >
> > _______________________________________________
> > Glasgow-haskell-users mailing list
> > Glasgow-haskell-users at haskell.org
> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> >
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20110214/5de3b11f/attachment.htm>