[Haskell-cafe] Advice on type families and non-injectivity?

[Simon Peyton-Jones]

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
Cc: Richard Eisenberg; glasgow-haskell-users at haskell.org; Haskell Cafe
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<mailto: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-----
| From: glasgow-haskell-users-bounces at haskell.org<mailto:glasgow-haskell-users-bounces at haskell.org> [mailto:glasgow-haskell-<mailto:glasgow-haskell->
| users-bounces at haskell.org<mailto:users-bounces at haskell.org>] On Behalf Of Richard Eisenberg
| Sent: 14 January 2013 03:47
| To: Conal Elliott
| Cc: glasgow-haskell-users at haskell.org<mailto:glasgow-haskell-users at haskell.org>; Haskell Cafe
| 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
| more information about your 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<mailto: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
| >
| > _______________________________________________
| > Glasgow-haskell-users mailing list
| > Glasgow-haskell-users at haskell.org<mailto:Glasgow-haskell-users at haskell.org>
| > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
|
|
| _______________________________________________
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users at haskell.org<mailto:Glasgow-haskell-users at haskell.org>
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130114/336b24d7/attachment.htm>