TypeFamilies vs. FunctionalDependencies & type-level recursion
dm-list-haskell-prime at scs.stanford.edu
dm-list-haskell-prime at scs.stanford.edu
Thu Jun 16 05:08:01 CEST 2011
At Wed, 15 Jun 2011 20:48:07 -0400,
Dan Doel wrote:
>
> I know that the actual, current implementation won't violate type
> safety. But there are reasonable expectations for how *functional
> dependencies* might work that would cause problems. Here's an example.
>
> class C a b | a -> b
>
> instance C Int b
>
> foo :: forall a b c d. (C a c, C b d, a ~ b) => a -> b -> c -> d
> foo _ _ x = x
>
> coerce :: forall a b. a -> b
> coerce = foo (5 :: Int) (5 :: Int)
>
> This currently gets complaints about not being able to deduce c ~ d.
> However, actually reading things as genuine functional dependencies,
> there's nothing wrong with the logic:
I don't understand how this code would work under any circumstances.
At the very least, you are missing a context for coerce and the type
of foo would have to be ... => a -> b -> c -> c. If two types are the
same, you are not allowed to declare them to be different.
Also, it's easy to add a method of some class to do the coercion,
while it's hard to emulate polymorphic types if you don't have them.
So I'd say the current behavior is more useful--allowing massive code
reduction in some cases, while I'm not yet convinced of the utility of
what you did above.
> instance (MonadState s m) => MonadState s (T m)
> ==>
> forall s m. (MSDict s m -> MSDict s (T m))
>
> And having access to
>
> forall s m. MSDict s (T m)
>
> is not at all the same as having access to
>
> forall m. MSDict (forall s. s) (T m)
I don't understand the difference, but admittedly I don't totally
follow your dictionary syntax. Recall the functional dependency goes
from right to left in this case: MonadState s m | m -> s, and
certainly the type forall m s. m -> s is equivalent to forall m. m ->
(forall s. s). It's only when the parentheses close before the last
argument that you need higher-rank types. But I think I'm probably
misunderstanding your example.
> > If, instead of FunctionalDependencies, the extension were called
> > ChooseInstancesWithoutKnowingAllTypeVariables, would you still have
> > this objection?
>
> No. In that case I would object that there are ad-hoc, unprincipled
> rules for resolving instances in GHC, and there should instead be some
> theoretical grounding to guide them. :)
Ah, we find agreement! I, too, am all in favor of rules with
theoretical grounding. The only thing I would add is that I don't
want to have to define N^2 instances for libraries like the mtl.
David
More information about the Haskell-prime
mailing list