Injective type families?

[Daniel Peebles]

I think what you want is closed type families, as do I and many others :)
Unfortunately we don't have those.

On Mon, Feb 14, 2011 at 10:02 PM, Conal Elliott <conal at conal.net> wrote:

> 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
>> >
>> >
>>
>
>
> _______________________________________________
> 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/1b62a28d/attachment.htm>