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 <simo...@microsoft.com>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-boun...@haskell.org [mailto: > glasgow-haskell-users- > | boun...@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 >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users