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 <co...@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
> <choe...@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 <co...@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
>
> > _______________________________________________
> > Glasgow-haskell-users mailing list
> > Glasgow-haskell-users@haskell.org
> > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
pgpQQPvW8QNiU.pgp
Description: PGP signature
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
