Re: Injective type families?

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 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 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