Advice on type families and non-injectivity?

[Conal Elliott]

>
> 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-----
> | From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-
> | 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; 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> 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
> | > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
> |
> |
> | _______________________________________________
> | Glasgow-haskell-users mailing list
> | 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/glasgow-haskell-users/attachments/20130114/3a38135d/attachment-0001.htm>