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

On Monday 14 February 2011 5:51:55 PM Daniel Peebles wrote:

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

Closed type families wouldn't necessarily be injective, either. What he wants is the facility to prove (or assert) to the compiler that a particualr type family is in fact injective. It's something that I haven't really even seen developed much in fancy dependently typed languages, though I've seen the idea before. That is: prove things about your program and have the compiler take advantage of it. -- Dan

Hello, shouldn't the check go the other way? (i.e., if the RHSs unify, then the LHS must be the same). Here is an example: -- This function is not injective. type instance F a = Int type instance F b = Int Still, Conal's example would not work if we just added support for injective type functions because + is not injective (e.g., 2 + 3 = 1 + 4). Instead, what we'd need to say is that it is injective in each argument separately, which would basically amount to adding functional dependencies to type functions. Perhaps something like this: type family (a :+: b) ~ c | c b -> a, c a -> b This seems like a feature which could be useful. -Iavor PS: Conal, I have been working on a GHC extension which has direct support for working with natural numbers at the type-level (e.g., + is a built-in type function which supports cancellation and other properties of the normal + operation). I am keen on collecting different ways in which people use type-level naturals to make sure that my implementation supports them (or at least report a decent error). I wasn't sure if the :+ from your example was just meant to illustrate the issue with injectivity, but if you have a use case for type nats, I'd be curious to find out more. On Mon, Feb 14, 2011 at 3:26 PM, Simon Peyton-Jones wrote:

Injective type families are a perfectly reasonable idea, but we have not implemented them (yet). The idea would be:

* You declare the family to be injective

injective type family T a :: *

* At every type instance, injectivity is checked. That is, if you say

type instance T (a,Int) = Either a Bool

then we must check that every type instance whose LHS unifies with this has the same RHS under the unifying substitution. Thus

type instance T (a,Bool) = [a] -- OK; does not unify type instance T (Int,b) = Either Int Bool -- OK; same RHS on (Int,Int)

I think it's mainly a question of tiresome design questions (notably do we want a new keyword "injective"? Should it go before "type"?) and hacking to get it all implemented.

Simon

| -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto: glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Dan Doel | Sent: 14 February 2011 23:14 | To: glasgow-haskell-users@haskell.org | Subject: Re: Injective type families? | | On Monday 14 February 2011 5:51:55 PM Daniel Peebles wrote: | > I think what you want is closed type families, as do I and many others :) | > Unfortunately we don't have those. | | Closed type families wouldn't necessarily be injective, either. What he wants | is the facility to prove (or assert) to the compiler that a particualr type | family is in fact injective. | | It's something that I haven't really even seen developed much in fancy | dependently typed languages, though I've seen the idea before. That is: prove | things about your program and have the compiler take advantage of it. | | -- Dan | | _______________________________________________ | 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

On Mon, Feb 14, 2011 at 1:41 PM, John Meacham wrote:

...

Isn't this what data families (as opposed to type families) do?

On Tue, Feb 15, 2011 at 7:02 AM, Conal Elliott wrote:

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

Roman Leshchinskiy once used a newtype to make a type family injective and remarked: "As an aside, it is well possible to [use] an injective data type family or even a GADT [instead]. ... However, this really messes up GHC’s optimiser and leads to very inefficient code." [1] Of course, introducing a newtype also requires introducing new types instead of reusing existing ones.. Sebastian [1]: http://unlines.wordpress.com/2010/11/15/generics-for-small-fixed-size-vector...