Quantcast

Injective type families?

classic Classic list List threaded Threaded
10 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Injective type families?

Conal Elliott
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
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Injective type families?

John Meacham
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
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Injective type families?

Conal Elliott
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 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
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

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



_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Injective type families?

Dan Doel
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
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

RE: Injective type families?

Simon Peyton Jones
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
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Injective type families?

Sebastian Fischer-2
In reply to this post by Conal Elliott
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


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Injective type families?

Iavor Diatchki
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:

* 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
|
|  _______________________________________________
|  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


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

RE: Injective type families?

Simon Peyton Jones

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
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Injective type families?

Roman Leshchinskiy
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
Loading...