Re: Fundeps and type equality

I don't think that's true (though a few minutes of searching has not yet turned up anything describing the original motivation for data families). Sometimes you really do want to construct a family of new data types, instead of just mapping to existing ones. I think everyone agrees that using data families as a stand-in for injective type families is a kludgy hack. -Brent On Wed, Dec 26, 2012 at 09:19:56PM +0200, Roman Cheplyaka wrote:

I presume that injectivity of type families is the sole reason why data families exist.

Roman

* Conal Elliott [2012-12-26 10:23:46-0800]

...

Hi Iavor,

Thanks much for the explanation.

Before this experiment with FDs, I was using a type family. I tried switching to FDs, because I wanted the compiler to know that the family is injective in order to assist type-checking. Can we declare type families to be injective? Now I see that I ran into a similar problem almost two years ago: http://haskell.1045720.n5.nabble.com/Injective-type-families-td3385084.html. I guess the answer is still "no", judging by this ticket: http://hackage.haskell.org/trac/ghc/ticket/6018 .

-- Conal

On Tue, Dec 25, 2012 at 6:47 PM, Iavor Diatchki wrote:

...

Hello Conal,

GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class).

As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest.

In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC.

Cheers, -Iavor PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet.

On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott wrote:

...

I ran into a simple falure with functional dependencies (in GHC 7.4.1):

...

class Foo a ta | a -> ta

foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool foo = (==)

I expected that the `a -> ta` functional dependency would suffice to prove that `ta ~ tb`, but

Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) => ta -> tb -> Bool at Pixie/Bug1.hs:9:1 Expected type: ta -> tb -> Bool Actual type: ta -> ta -> Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none.

Any insights about what's going wrong here?

-- Conal

_______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

...

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users