Advice on type families and noninjectivity?
Simon PeytonJones
simonpj at microsoft.com
Mon Jan 14 22:19:46 CET 2013
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 PeytonJones
Cc: Richard Eisenberg; glasgowhaskellusers at haskell.org; Haskell Cafe
Subject: Re: Advice on type families and noninjectivity?
There is a real difficulty here with typechecking '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 PeytonJones <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 typechecking '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: glasgowhaskellusersbounces at haskell.org<mailto:glasgowhaskellusersbounces at haskell.org> [mailto:glasgowhaskell<mailto:glasgowhaskell>
 usersbounces at haskell.org<mailto:usersbounces at haskell.org>] On Behalf Of Richard Eisenberg
 Sent: 14 January 2013 03:47
 To: Conal Elliott
 Cc: glasgowhaskellusers at haskell.org<mailto:glasgowhaskellusers at haskell.org>; Haskell Cafe
 Subject: Re: Advice on type families and noninjectivity?

 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 workarounds.
 >
 > I know about (injective) data families but don't want to lose the
 convenience of type synonym families.
 >
 > Thanks,  Conal
 >
 > _______________________________________________
 > Glasgowhaskellusers mailing list
 > Glasgowhaskellusers at haskell.org<mailto:Glasgowhaskellusers at haskell.org>
 > http://www.haskell.org/mailman/listinfo/glasgowhaskellusers


 _______________________________________________
 Glasgowhaskellusers mailing list
 Glasgowhaskellusers at haskell.org<mailto:Glasgowhaskellusers at haskell.org>
 http://www.haskell.org/mailman/listinfo/glasgowhaskellusers
 next part 
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgowhaskellusers/attachments/20130114/336b24d7/attachment0001.htm>
More information about the Glasgowhaskellusers
mailing list