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 [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
Isn't this what data families (as opposed to type families) do?
John On Mon, Feb 14, 2011 at 1:28 PM, Conal Elliott <[hidden email]> 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 > [hidden email] > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
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 <[hidden email]> wrote: Isn't this what data families (as opposed to type families) do? _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
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 <[hidden email]> wrote: Yes, it's one things that data families do. Another is introducing *new* data types rather than reusing existing ones. - Conal _______________________________________________ Glasgow-haskell-users mailing list [hidden email] 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 _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
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: [hidden email] [mailto:glasgow-haskell-users- | [hidden email]] On Behalf Of Dan Doel | Sent: 14 February 2011 23:14 | To: [hidden email] | 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 | [hidden email] | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Conal Elliott
On Tue, Feb 15, 2011 at 7:02 AM, Conal Elliott <[hidden email]> 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 _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Simon Peyton Jones
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 <[hidden email]> wrote: Injective type families are a perfectly reasonable idea, but we have not implemented them (yet). The idea would be: _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
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 Yes, you’re right. 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 Interesting! Injectivity is more complicated than one might think!
Simon _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
In reply to this post by Conal Elliott
On 14/02/2011, at 21:28, 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) You could prove it :-) class Nat n where induct :: p Z -> (forall m. p m -> p (S m)) -> p n instance Nat Z where induct z _ = z instance Nat n => Nat (S n) where induct z s = s (induct z s) data P n1 n2 m where P :: (forall a. (m :+: n1) ~ (m :+: n2) => (n1 ~ n2 => a) -> a) -> P n1 n2 m injective :: forall m n1 n2 a. (Nat m, (m :+: n1) ~ (m :+: n2)) => n1 -> n2 -> m -> (n1 ~ n2 => a) -> a injective _ _ _ x = case induct (P (\x -> x)) (\(P f) -> P f) :: P n1 n2 m of P f -> f x This is a bit inefficient, of course, because it involves recursion. With a little bit of safe cheating, it is possible to get by without recursion, basically by making induction an axiom rather than "proving" it. It would be nicer if the compiler could prove it for us, of course. Roman _______________________________________________ Glasgow-haskell-users mailing list [hidden email] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users |
Powered by Nabble | Edit this page |