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 <j...@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 <co...@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@haskell.org > > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > > > >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
