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 [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 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 [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