13 Jan 2013 20:10

Advice on type families and non-injectivity?

I sometimes run into trouble with lack of injectivity for type families. I'm trying to understand what's at the heart of these difficulties and whether I can avoid them. Also, whether some of the obstacles could be overcome with simple improvements to GHC.

Here's a simple example:

> {-# LANGUAGE TypeFamilies #-}
>
> type family F a
>
> foo :: F a
> foo = undefined
>
> bar :: F a
> bar = foo

The error message:

Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo

A terser (but perhaps subtler) example producing the same error:

> baz :: F a
> baz = baz

Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.

Does the difficulty here have to do with trying to *infer* the type and then compare with the given one? Or is there an issue even with type *checking* in such cases?

Other insights welcome, as well as suggested work-arounds.

I know about (injective) data families but don't want to lose the convenience of type synonym families.

Thanks,  -- Conal

```_______________________________________________
```
13 Jan 2013 20:36

Re: Advice on type families and non-injectivity?

```Hi,

How would you infer "a" from "F a"? Given "bar :: Bool", I can't see how
one could go from "Bool" to "F a = Bool" and determine "a" uniquely.

My question is not completely retorical, if there is an answer I would
like to know it

Gruss,
Christian

* Conal Elliott <conal <at> conal.net> [13.01.2013 20:13]:
>    I sometimes run into trouble with lack of injectivity for type families.
>    I'm trying to understand what's at the heart of these difficulties and
>    whether I can avoid them. Also, whether some of the obstacles could be
>    overcome with simple improvements to GHC.
>
>    Here's a simple example:
>
>    > {-# LANGUAGE TypeFamilies #-}
>    >
>    > type family F a
>    >
>    > foo :: F a
>    > foo = undefined
>    >
>    > bar :: F a
>    > bar = foo
>
>    The error message:
>
>        Couldn't match type `F a' with `F a1'
>        NB: `F' is a type function, and may not be injective
>        In the expression: foo
>        In an equation for `bar': bar = foo
>
>    A terser (but perhaps subtler) example producing the same error:
>
>    > baz :: F a
>    > baz = baz
>
>    Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
>
>    Does the difficulty here have to do with trying to *infer* the type and
>    then compare with the given one? Or is there an issue even with type
>    *checking* in such cases?
>
>    Other insights welcome, as well as suggested work-arounds.
>
>    I know about (injective) data families but don't want to lose the
>    convenience of type synonym families.
>
>    Thanks,  -- Conal

> _______________________________________________

```
```_______________________________________________
```
13 Jan 2013 21:13

Re: Advice on type families and non-injectivity?

Hi Christian,

Given "bar :: Bool", I can't see how one could go from "Bool" to "F a = Bool" and determine "a" uniquely.

The same question applies to "foo :: Bool", right? Yet no error message there.

Regards, - Conal

On Sun, Jan 13, 2013 at 11:36 AM, Christian Höner zu Siederdissen wrote:
Hi,

How would you infer "a" from "F a"? Given "bar :: Bool", I can't see how
one could go from "Bool" to "F a = Bool" and determine "a" uniquely.

My question is not completely retorical, if there is an answer I would
like to know it

Gruss,
Christian

* Conal Elliott <conal <at> conal.net> [13.01.2013 20:13]:
>    I sometimes run into trouble with lack of injectivity for type families.
>    I'm trying to understand what's at the heart of these difficulties and
>    whether I can avoid them. Also, whether some of the obstacles could be
>    overcome with simple improvements to GHC.
>
>    Here's a simple example:
>
>    > {-# LANGUAGE TypeFamilies #-}
>    >
>    > type family F a
>    >
>    > foo :: F a
>    > foo = undefined
>    >
>    > bar :: F a
>    > bar = foo
>
>    The error message:
>
>        Couldn't match type `F a' with `F a1'
>        NB: `F' is a type function, and may not be injective
>        In the expression: foo
>        In an equation for `bar': bar = foo
>
>    A terser (but perhaps subtler) example producing the same error:
>
>    > baz :: F a
>    > baz = baz
>
>    Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
>
>    Does the difficulty here have to do with trying to *infer* the type and
>    then compare with the given one? Or is there an issue even with type
>    *checking* in such cases?
>
>    Other insights welcome, as well as suggested work-arounds.
>
>    I know about (injective) data families but don't want to lose the
>    convenience of type synonym families.
>
>    Thanks,  -- Conal

> _______________________________________________

```_______________________________________________
```
14 Jan 2013 00:20

Re: Advice on type families and non-injectivity?

```Hi Conal,

if you take your example program and write "foo :: Bool", ghci accepts it?

For me it complains, and I would think rightly so, that "couldn't match
expected type Fa with actual type Bool". It actually only works with the
following quite useless "type instance F a = Bool".

By the way, using above instance, the original example works...

Ultimatively, injective type families would be useful. Thinking about
roman's vector library for example. For my code, I am switching more and
more to data families to get the desired behaviour of: F a ~ F b => a ~ b

Gruss,
Christian

* Conal Elliott <conal <at> conal.net> [13.01.2013 21:14]:
>    Hi Christian,
>
>      Given "bar :: Bool", I can't see how one could go from "Bool" to "F a =
>      Bool" and determine "a" uniquely.
>
>    The same question applies to "foo :: Bool", right? Yet no error message
>    there.
>
>    Regards, - Conal
>    On Sun, Jan 13, 2013 at 11:36 AM, Christian Ho:ner zu Siederdissen
>    <choener <at> tbi.univie.ac.at> wrote:
>
>      Hi,
>
>      How would you infer "a" from "F a"? Given "bar :: Bool", I can't see how
>      one could go from "Bool" to "F a = Bool" and determine "a" uniquely.
>
>      My question is not completely retorical, if there is an answer I would
>      like to know it
>
>      Gruss,
>      Christian
>
>      * Conal Elliott <conal <at> conal.net> [13.01.2013 20:13]:
>      >    I sometimes run into trouble with lack of injectivity for type
>      families.
>      >    I'm trying to understand what's at the heart of these difficulties
>      and
>      >    whether I can avoid them. Also, whether some of the obstacles could
>      be
>      >    overcome with simple improvements to GHC.
>      >
>      >    Here's a simple example:
>      >
>      >    > {-# LANGUAGE TypeFamilies #-}
>      >    >
>      >    > type family F a
>      >    >
>      >    > foo :: F a
>      >    > foo = undefined
>      >    >
>      >    > bar :: F a
>      >    > bar = foo
>      >
>      >    The error message:
>      >
>      >        Couldn't match type `F a' with `F a1'
>      >        NB: `F' is a type function, and may not be injective
>      >        In the expression: foo
>      >        In an equation for `bar': bar = foo
>      >
>      >    A terser (but perhaps subtler) example producing the same error:
>      >
>      >    > baz :: F a
>      >    > baz = baz
>      >
>      >    Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
>      >
>      >    Does the difficulty here have to do with trying to *infer* the type
>      and
>      >    then compare with the given one? Or is there an issue even with
>      type
>      >    *checking* in such cases?
>      >
>      >    Other insights welcome, as well as suggested work-arounds.
>      >
>      >    I know about (injective) data families but don't want to lose the
>      >    convenience of type synonym families.
>      >
>      >    Thanks,  -- Conal
>
>      > _______________________________________________
```
```_______________________________________________
```
13 Jan 2013 20:39

Re: Advice on type families and non-injectivity?

Hello Conal,

The issue with your example is that it is ambiguous, so GHC can't figure out how to instantiate the use of `foo`.   It might be easier to see why this is if you write it in this form:

> foo :: (F a ~ b) => b
> foo = ...

Now, we can see that only `b` appears on the RHS of the `=>`, so there is really no way for GHC to figure out what is the intended value for `a`.  Replacing `a` with a concrete type (such as `Bool`) eliminates the problem, because now GHC does not need to come up with a value for `a`.   Another way to eliminate the ambiguity would be if `F` was injective---then we'd know that `b` uniquely determines `a` so again there would be no ambiguity.

If `F` is not injective, however, the only workaround would be to write the type in such a way that the function arguments appear in the signature directly (e.g., something like 'a -> F a' would be ok).

-Iavor

On Sun, Jan 13, 2013 at 11:10 AM, Conal Elliott wrote:
I sometimes run into trouble with lack of injectivity for type families. I'm trying to understand what's at the heart of these difficulties and whether I can avoid them. Also, whether some of the obstacles could be overcome with simple improvements to GHC.

Here's a simple example:

> {-# LANGUAGE TypeFamilies #-}
>
> type family F a
>
> foo :: F a
> foo = undefined
>
> bar :: F a
> bar = foo

The error message:

Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo

A terser (but perhaps subtler) example producing the same error:

> baz :: F a
> baz = baz

Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.

Does the difficulty here have to do with trying to *infer* the type and then compare with the given one? Or is there an issue even with type *checking* in such cases?

Other insights welcome, as well as suggested work-arounds.

I know about (injective) data families but don't want to lose the convenience of type synonym families.

Thanks,  -- Conal

_______________________________________________

```_______________________________________________
```
13 Jan 2013 21:05

Re: Advice on type families and non-injectivity?

Hi Iavor,

Thanks for the remarks.

so there is really no way for GHC to figure out what is the intended value for `a`.

Indeed. Though I wonder: does the type-checker really need to find a binding for `a` in this case, i.e., given the equation `(forall a. F a) == (forall a'. F a')`?

-- Conal

On Sun, Jan 13, 2013 at 11:39 AM, Iavor Diatchki wrote:
Hello Conal,

The issue with your example is that it is ambiguous, so GHC can't figure out how to instantiate the use of `foo`.   It might be easier to see why this is if you write it in this form:

> foo :: (F a ~ b) => b
> foo = ...

Now, we can see that only `b` appears on the RHS of the `=>`, so there is really no way for GHC to figure out what is the intended value for `a`.  Replacing `a` with a concrete type (such as `Bool`) eliminates the problem, because now GHC does not need to come up with a value for `a`.   Another way to eliminate the ambiguity would be if `F` was injective---then we'd know that `b` uniquely determines `a` so again there would be no ambiguity.

If `F` is not injective, however, the only workaround would be to write the type in such a way that the function arguments appear in the signature directly (e.g., something like 'a -> F a' would be ok).

-Iavor

On Sun, Jan 13, 2013 at 11:10 AM, Conal Elliott wrote:
I sometimes run into trouble with lack of injectivity for type families. I'm trying to understand what's at the heart of these difficulties and whether I can avoid them. Also, whether some of the obstacles could be overcome with simple improvements to GHC.

Here's a simple example:

> {-# LANGUAGE TypeFamilies #-}
>
> type family F a
>
> foo :: F a
> foo = undefined
>
> bar :: F a
> bar = foo

The error message:

Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo

A terser (but perhaps subtler) example producing the same error:

> baz :: F a
> baz = baz

Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.

Does the difficulty here have to do with trying to *infer* the type and then compare with the given one? Or is there an issue even with type *checking* in such cases?

Other insights welcome, as well as suggested work-arounds.

I know about (injective) data families but don't want to lose the convenience of type synonym families.

Thanks,  -- Conal

_______________________________________________

```_______________________________________________
```
13 Jan 2013 21:52

Re: Advice on type families and non-injectivity?

Hello,

On Sun, Jan 13, 2013 at 12:05 PM, Conal Elliott wrote:

so there is really no way for GHC to figure out what is the intended value for `a`.

Indeed. Though I wonder: does the type-checker really need to find a binding for `a` in this case, i.e., given the equation `(forall a. F a) == (forall a'. F a')`?

Wouldn't that make `F` a constant type family, and so one could just skip the `a` parameter?   Anyway, if there was a way to assert something like that about a type-function, than there would be no problem.   When something like that happens (i.e., GHC figures out that it does not know how to instantiate a type variable, but it is sure that the actual instantiation does not matter), GHC instantiates the variable a special type called `Any`, which has a very polymorphic kind.

By the way, Simon recently reworked the ambiguity checker in GHC, and now HEAD correctly rejects `foo` as being ambiguous (the new ambiguity check uses exactly what's in your example: a value `f :: S` is ambiguous, if `g :: S; g = f` results in an error).

-Iavor

```_______________________________________________
```
14 Jan 2013 00:53

Re: Advice on type families and non-injectivity?

```On 1/13/13 3:52 PM, Iavor Diatchki wrote:
> On Sun, Jan 13, 2013 at 12:05 PM, Conal Elliott <conal <at> conal.net> wrote:
>>> so there is really no way for GHC to figure out what is the intended value
>>> for `a`.
>>
>> Indeed. Though I wonder: does the type-checker really need to find a
>> binding for `a` in this case, i.e., given the equation `(forall a. F a) ==
>> (forall a'. F a')`?
>
> Wouldn't that make `F` a constant type family,

I don't see why. If we translate this to dependent type notation we get:

((a::*) -> F a) == ((b::*) -> F b)

This equality should hold in virtue of alpha-conversion. What F is, is
irrelevant; the only thing that matters is that it has kind *->*. In
particular, it doesn't matter whether F is arbitrary, injective,
parametric, constant, etc.

The problem is that the above isn't the equation GHC sees. GHC sees:

F a == F b

and it can't infer any correlation between a and b, where one of those
is universally quantified in the context (the definition of bar) and the
other is something we need to fabricate to hand off to the polymorphic
value (the call to foo).

Of course, in this particular case it *ought* to be fine, by
parametricity in the definition of foo. That is, since we merely need to
come up with some b, any b, such that F b is the type we need (namely: F
a), the a we have will suffice for that. So if we're explicit about type
passing, the following is fine:

foo :: forall b. F b

bar :: forall a. F a
bar = /\a -> foo  <at> a

The problem is that while the a is sufficient it's not (in general)
necessary. And that's the ambiguity GHC is complaining about. GHC can't
see that foo is parametric in b, and therefore that a is as good as any
other type.

--

--
Live well,
~wren
```
13 Jan 2013 22:59

Re: Advice on type families and non-injectivity?

I have a trick that loses a little convenience, but may still be more convenient than data families.

{-# LANGUAGE TypeFamilies #-}

import Data.Tagged

type family F a

foo :: Tagged a (F a)
foo = Tagged undefined

bar :: Tagged a (F a)
bar = foo

This allows you to use the same newtype wrapper consistently, regardless of what the type instance actually is; one of the inconveniences of data families is the need to use different constructors for different types.

On Sun, Jan 13, 2013 at 2:10 PM, Conal Elliott wrote:
I sometimes run into trouble with lack of injectivity for type families. I'm trying to understand what's at the heart of these difficulties and whether I can avoid them. Also, whether some of the obstacles could be overcome with simple improvements to GHC.

Here's a simple example:

> {-# LANGUAGE TypeFamilies #-}
>
> type family F a
>
> foo :: F a
> foo = undefined
>
> bar :: F a
> bar = foo

The error message:

Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo

A terser (but perhaps subtler) example producing the same error:

> baz :: F a
> baz = baz

Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.

Does the difficulty here have to do with trying to *infer* the type and then compare with the given one? Or is there an issue even with type *checking* in such cases?

Other insights welcome, as well as suggested work-arounds.

I know about (injective) data families but don't want to lose the convenience of type synonym families.

Thanks,  -- Conal

_______________________________________________

```_______________________________________________
```
14 Jan 2013 21:53

Thanks, Jake! This suggestion helped a lot.  -- Conal

On Sun, Jan 13, 2013 at 1:59 PM, Jake McArthur wrote:
I have a trick that loses a little convenience, but may still be more convenient than data families.

{-# LANGUAGE TypeFamilies #-}

import Data.Tagged

type family F a

foo :: Tagged a (F a)
foo = Tagged undefined

bar :: Tagged a (F a)
bar = foo

This allows you to use the same newtype wrapper consistently, regardless of what the type instance actually is; one of the inconveniences of data families is the need to use different constructors for different types.

On Sun, Jan 13, 2013 at 2:10 PM, Conal Elliott wrote:
I sometimes run into trouble with lack of injectivity for type families. I'm trying to understand what's at the heart of these difficulties and whether I can avoid them. Also, whether some of the obstacles could be overcome with simple improvements to GHC.

Here's a simple example:

> {-# LANGUAGE TypeFamilies #-}
>
> type family F a
>
> foo :: F a
> foo = undefined
>
> bar :: F a
> bar = foo

The error message:

Couldn't match type `F a' with `F a1'
NB: `F' is a type function, and may not be injective
In the expression: foo
In an equation for `bar': bar = foo

A terser (but perhaps subtler) example producing the same error:

> baz :: F a
> baz = baz

Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.

Does the difficulty here have to do with trying to *infer* the type and then compare with the given one? Or is there an issue even with type *checking* in such cases?

Other insights welcome, as well as suggested work-arounds.

I know about (injective) data families but don't want to lose the convenience of type synonym families.

Thanks,  -- Conal

_______________________________________________

```_______________________________________________
```
14 Jan 2013 04:46

Re: Advice on type families and non-injectivity?

```Hi Conal,

I agree that your initial example is a little puzzling, and I'm glad that the new ambiguity checker prevents
both definitions, not just one.

However, your initial question seems broader than just this example. I have run into this problem (wanting
injective type functions) several times myself, and have been successful at finding workarounds. But, I
problem, perhaps I or others can contribute.

For what it's worth, the desire for injective type functions has been entered as ticket #6018 in the GHC
Trac, but I see you're already on the cc: list. I believe Simon PJ has given serious thought to implementing
this feature and may have even put in some very basic code toward this end.

Richard

On Jan 13, 2013, at 2:10 PM, Conal Elliott <conal <at> conal.net> wrote:

> I sometimes run into trouble with lack of injectivity for type families. I'm trying to understand what's
at the heart of these difficulties and whether I can avoid them. Also, whether some of the obstacles could
be overcome with simple improvements to GHC.
>
> Here's a simple example:
>
> > {-# LANGUAGE TypeFamilies #-}
> >
> > type family F a
> >
> > foo :: F a
> > foo = undefined
> >
> > bar :: F a
> > bar = foo
>
> The error message:
>
>     Couldn't match type `F a' with `F a1'
>     NB: `F' is a type function, and may not be injective
>     In the expression: foo
>     In an equation for `bar': bar = foo
>
> A terser (but perhaps subtler) example producing the same error:
>
> > baz :: F a
> > baz = baz
>
> Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
>
> Does the difficulty here have to do with trying to *infer* the type and then compare with the given one? Or is
there an issue even with type *checking* in such cases?
>
> Other insights welcome, as well as suggested work-arounds.
>
> I know about (injective) data families but don't want to lose the convenience of type synonym families.
>
> Thanks,  -- Conal
>
> _______________________________________________
```
14 Jan 2013 12:39

RE: Advice on type families and non-injectivity?

```| > > {-# LANGUAGE TypeFamilies #-}
| > >
| > > type family F a
| > >
| > > foo :: F a
| > > foo = undefined
| > >
| > > bar :: F a
| > > bar = foo

There is a real difficulty here with type-checking 'bar'.  (And that difficulty is why 'foo' is also rejected.)

Namely, when typechecking 'bar', we must instantiate foo with an unknown type, say alpha.  So now we must
find a type 'alpha' such that
F a ~ F alpha
Certainly alpha=1 is one solution, but there might be others.  For example, suppose
type instance F [b] = F b
Then alpha=[a] would also be a solution.

In this particular case any solution will do, but suppose there was an addition constraint (C alpha)
arising from the right hand side, where C is a class.  Then if we had
instance C [b] where ...
then the second solution (alpha=[a]) would work, but not the first.  This can get arbitrarily complicated,
and GHC's type inference does not "search" various solutions; it follows one path.

The solution is to provide a way to fix alpha. For example,
foo :: a -> F a
is fine.

Simon

| -----Original Message-----
| users-bounces <at> haskell.org] On Behalf Of Richard Eisenberg
| Sent: 14 January 2013 03:47
| To: Conal Elliott
| Subject: Re: Advice on type families and non-injectivity?
|
| Hi Conal,
|
| I agree that your initial example is a little puzzling, and I'm glad
| that the new ambiguity checker prevents both definitions, not just one.
|
| However, your initial question seems broader than just this example. I
| have run into this problem (wanting injective type functions) several
| times myself, and have been successful at finding workarounds. But, I
| can't think of any unifying principle or solid advice. If you can post
|
| For what it's worth, the desire for injective type functions has been
| entered as ticket #6018 in the GHC Trac, but I see you're already on the
| cc: list. I believe Simon PJ has given serious thought to implementing
| this feature and may have even put in some very basic code toward this
| end.
|
| Richard
|
| On Jan 13, 2013, at 2:10 PM, Conal Elliott <conal <at> conal.net> wrote:
|
| > I sometimes run into trouble with lack of injectivity for type
| families. I'm trying to understand what's at the heart of these
| difficulties and whether I can avoid them. Also, whether some of the
| obstacles could be overcome with simple improvements to GHC.
| >
| > Here's a simple example:
| >
| > > {-# LANGUAGE TypeFamilies #-}
| > >
| > > type family F a
| > >
| > > foo :: F a
| > > foo = undefined
| > >
| > > bar :: F a
| > > bar = foo
| >
| > The error message:
| >
| >     Couldn't match type `F a' with `F a1'
| >     NB: `F' is a type function, and may not be injective
| >     In the expression: foo
| >     In an equation for `bar': bar = foo
| >
| > A terser (but perhaps subtler) example producing the same error:
| >
| > > baz :: F a
| > > baz = baz
| >
| > Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
| >
| > Does the difficulty here have to do with trying to *infer* the type
| and then compare with the given one? Or is there an issue even with type
| *checking* in such cases?
| >
| > Other insights welcome, as well as suggested work-arounds.
| >
| > I know about (injective) data families but don't want to lose the
| convenience of type synonym families.
| >
| > Thanks,  -- Conal
| >
| > _______________________________________________
|
|
| _______________________________________________
```
14 Jan 2013 21:51

Re: Advice on type families and non-injectivity?

There is a real difficulty here with type-checking 'bar'.  (And that difficulty is why 'foo' is also rejected.)

Oh! Is the definition of 'foo' rejected in recent versions of GHC? My 7.4.1 installation doesn't complain.   -- Conal

On Mon, Jan 14, 2013 at 3:39 AM, Simon Peyton-Jones wrote:
| > > {-# LANGUAGE TypeFamilies #-}
| > >
| > > type family F a
| > >
| > > foo :: F a
| > > foo = undefined
| > >
| > > bar :: F a
| > > bar = foo

There is a real difficulty here with type-checking 'bar'.  (And that difficulty is why 'foo' is also rejected.)

Namely, when typechecking 'bar', we must instantiate foo with an unknown type, say alpha.  So now we must find a type 'alpha' such that
F a ~ F alpha
Certainly alpha=1 is one solution, but there might be others.  For example, suppose
type instance F [b] = F b
Then alpha=[a] would also be a solution.

In this particular case any solution will do, but suppose there was an addition constraint (C alpha) arising from the right hand side, where C is a class.  Then if we had
instance C [b] where ...
then the second solution (alpha=[a]) would work, but not the first.  This can get arbitrarily complicated, and GHC's type inference does not "search" various solutions; it follows one path.

The solution is to provide a way to fix alpha. For example,
foo :: a -> F a
is fine.

Simon

| -----Original Message-----
| users-bounces <at> haskell.org] On Behalf Of Richard Eisenberg
| Sent: 14 January 2013 03:47
| To: Conal Elliott
| Subject: Re: Advice on type families and non-injectivity?
|
| Hi Conal,
|
| I agree that your initial example is a little puzzling, and I'm glad
| that the new ambiguity checker prevents both definitions, not just one.
|
| However, your initial question seems broader than just this example. I
| have run into this problem (wanting injective type functions) several
| times myself, and have been successful at finding workarounds. But, I
| can't think of any unifying principle or solid advice. If you can post
|
| For what it's worth, the desire for injective type functions has been
| entered as ticket #6018 in the GHC Trac, but I see you're already on the
| cc: list. I believe Simon PJ has given serious thought to implementing
| this feature and may have even put in some very basic code toward this
| end.
|
| Richard
|
| On Jan 13, 2013, at 2:10 PM, Conal Elliott <conal <at> conal.net> wrote:
|
| > I sometimes run into trouble with lack of injectivity for type
| families. I'm trying to understand what's at the heart of these
| difficulties and whether I can avoid them. Also, whether some of the
| obstacles could be overcome with simple improvements to GHC.
| >
| > Here's a simple example:
| >
| > > {-# LANGUAGE TypeFamilies #-}
| > >
| > > type family F a
| > >
| > > foo :: F a
| > > foo = undefined
| > >
| > > bar :: F a
| > > bar = foo
| >
| > The error message:
| >
| >     Couldn't match type `F a' with `F a1'
| >     NB: `F' is a type function, and may not be injective
| >     In the expression: foo
| >     In an equation for `bar': bar = foo
| >
| > A terser (but perhaps subtler) example producing the same error:
| >
| > > baz :: F a
| > > baz = baz
| >
| > Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
| >
| > Does the difficulty here have to do with trying to *infer* the type
| and then compare with the given one? Or is there an issue even with type
| *checking* in such cases?
| >
| > Other insights welcome, as well as suggested work-arounds.
| >
| > I know about (injective) data families but don't want to lose the
| convenience of type synonym families.
| >
| > Thanks,  -- Conal
| >
| > _______________________________________________
|
|
| _______________________________________________

```_______________________________________________
```
14 Jan 2013 22:19

RE: Advice on type families and non-injectivity?

Oh! Is the definition of 'foo' rejected in recent versions of GHC? My 7.4.1 installation doesn't complain.   -- Conal

Yes, it is rejected.

Simon

From: conal.elliott <at> gmail.com [mailto:conal.elliott <at> gmail.com] On Behalf Of Conal Elliott
Sent: 14 January 2013 20:52
To: Simon Peyton-Jones
Subject: Re: Advice on type families and non-injectivity?

There is a real difficulty here with type-checking 'bar'.  (And that difficulty is why 'foo' is also rejected.)

Oh! Is the definition of 'foo' rejected in recent versions of GHC? My 7.4.1 installation doesn't complain.   -- Conal

On Mon, Jan 14, 2013 at 3:39 AM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

| > > {-# LANGUAGE TypeFamilies #-}
| > >
| > > type family F a
| > >
| > > foo :: F a
| > > foo = undefined
| > >
| > > bar :: F a
| > > bar = foo

There is a real difficulty here with type-checking 'bar'.  (And that difficulty is why 'foo' is also rejected.)

Namely, when typechecking 'bar', we must instantiate foo with an unknown type, say alpha.  So now we must find a type 'alpha' such that
F a ~ F alpha
Certainly alpha=1 is one solution, but there might be others.  For example, suppose
type instance F [b] = F b
Then alpha=[a] would also be a solution.

In this particular case any solution will do, but suppose there was an addition constraint (C alpha) arising from the right hand side, where C is a class.  Then if we had
instance C [b] where ...
then the second solution (alpha=[a]) would work, but not the first.  This can get arbitrarily complicated, and GHC's type inference does not "search" various solutions; it follows one path.

The solution is to provide a way to fix alpha. For example,
foo :: a -> F a
is fine.

Simon

| -----Original Message-----
| users-bounces <at> haskell.org] On Behalf Of Richard Eisenberg
| Sent: 14 January 2013 03:47
| To: Conal Elliott
| Subject: Re: Advice on type families and non-injectivity?
|
| Hi Conal,
|
| I agree that your initial example is a little puzzling, and I'm glad
| that the new ambiguity checker prevents both definitions, not just one.
|
| However, your initial question seems broader than just this example. I
| have run into this problem (wanting injective type functions) several
| times myself, and have been successful at finding workarounds. But, I
| can't think of any unifying principle or solid advice. If you can post
|
| For what it's worth, the desire for injective type functions has been
| entered as ticket #6018 in the GHC Trac, but I see you're already on the
| cc: list. I believe Simon PJ has given serious thought to implementing
| this feature and may have even put in some very basic code toward this
| end.
|
| Richard
|
| On Jan 13, 2013, at 2:10 PM, Conal Elliott <conal <at> conal.net> wrote:
|
| > I sometimes run into trouble with lack of injectivity for type
| families. I'm trying to understand what's at the heart of these
| difficulties and whether I can avoid them. Also, whether some of the
| obstacles could be overcome with simple improvements to GHC.
| >
| > Here's a simple example:
| >
| > > {-# LANGUAGE TypeFamilies #-}
| > >
| > > type family F a
| > >
| > > foo :: F a
| > > foo = undefined
| > >
| > > bar :: F a
| > > bar = foo
| >
| > The error message:
| >
| >     Couldn't match type `F a' with `F a1'
| >     NB: `F' is a type function, and may not be injective
| >     In the expression: foo
| >     In an equation for `bar': bar = foo
| >
| > A terser (but perhaps subtler) example producing the same error:
| >
| > > baz :: F a
| > > baz = baz
| >
| > Replacing `a` with a monotype (e.g., `Bool`) eliminates the error.
| >
| > Does the difficulty here have to do with trying to *infer* the type
| and then compare with the given one? Or is there an issue even with type
| *checking* in such cases?
| >
| > Other insights welcome, as well as suggested work-arounds.
| >
| > I know about (injective) data families but don't want to lose the
| convenience of type synonym families.
| >
| > Thanks,  -- Conal
| >
| > _______________________________________________
|
|
| _______________________________________________

```_______________________________________________
```
14 Jan 2013 21:59

Re: Advice on type families and non-injectivity?

```On Mon, Jan 14, 2013 at 3:39 AM, Simon Peyton-Jones
<simonpj <at> microsoft.com> wrote:
> There is a real difficulty here with type-checking 'bar'.  (And that
> difficulty is why 'foo' is also rejected.)

This seems, to me, like a somewhat round-about way to express the
problem.  Iavor's explanation (which approach I have also found useful
to explain the behavior of type functions in the past) captures the
ambiguity in both descriptions:

> foo :: (T a ~ b) => b
> foo = undefined

That this is ambiguous should be obvious.  Accepting such a definition
could presumably be used to generate values of undefined type; for
example, I could get a generic instance

> foo :: T Int

whether or not T Int is defined in my program!  This also, to me, seems
to make it clear that past GHC's acceptance of foo was in error.

/g

--
Sent from my mail client.
```

Gmane