Advice on type families and non-injectivity?

[Christian Höner zu Siederdissen]

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 <conal at 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
>    <choener at 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 <conal at 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 at haskell.org
>      > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20130114/a23258d7/attachment.pgp>