

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 righthand sides.
Since this example is fairly common, I wonder: does anyone have a trick for avoiding the injectivity issue? Thanks,  Conal
_______________________________________________
Glasgowhaskellusers mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgowhaskellusers


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 righthand sides.
>
> Since this example is fairly common, I wonder: does anyone have a trick for
> avoiding the injectivity issue?
>
> Thanks,  Conal
>
> _______________________________________________
> Glasgowhaskellusers mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgowhaskellusers>
>
_______________________________________________
Glasgowhaskellusers mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgowhaskellusers


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?
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 righthand sides.
>
> Since this example is fairly common, I wonder: does anyone have a trick for
> avoiding the injectivity issue?
>
> Thanks,  Conal
>
> _______________________________________________
> Glasgowhaskellusers mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
>
>
_______________________________________________
Glasgowhaskellusers mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgowhaskellusers


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
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?
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 righthand sides.
>
> Since this example is fairly common, I wonder: does anyone have a trick for
> avoiding the injectivity issue?
>
> Thanks,  Conal
>
> _______________________________________________
> Glasgowhaskellusers mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
>
>
_______________________________________________
Glasgowhaskellusers mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
_______________________________________________
Glasgowhaskellusers mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgowhaskellusers


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
_______________________________________________
Glasgowhaskellusers mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgowhaskellusers


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:glasgowhaskellusers
 [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

 _______________________________________________
 Glasgowhaskellusers mailing list
 [hidden email]
 http://www.haskell.org/mailman/listinfo/glasgowhaskellusers_______________________________________________
Glasgowhaskellusers mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgowhaskellusers


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? 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
_______________________________________________
Glasgowhaskellusers mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgowhaskellusers


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 typelevel (e.g., + is a builtin type function which supports cancellation and other properties of the normal + operation). I am keen on collecting different ways in which people use typelevel 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 PeytonJones <[hidden email]> 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: [hidden email] [mailto: [hidden email]
 [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

 _______________________________________________
 Glasgowhaskellusers mailing list
 [hidden email]
 http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
_______________________________________________
Glasgowhaskellusers mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
_______________________________________________
Glasgowhaskellusers mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgowhaskellusers


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.
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
_______________________________________________
Glasgowhaskellusers mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgowhaskellusers


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
_______________________________________________
Glasgowhaskellusers mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgowhaskellusers

