TypeFamilies vs. FunctionalDependencies & type-level recursion
Dan Doel
dan.doel at gmail.com
Wed Jun 15 01:21:38 CEST 2011
On Tue, Jun 14, 2011 at 5:38 PM,
<dm-list-haskell-prime at scs.stanford.edu> wrote:
> Undecidable instances are orthogonal to both FunctionalDependencies
> and OverlappingInstances. They concern whether or not the compiler
> can guarantee that the typechecker will terminate. You can have
> undecidable instances without either of the other two extensions
I'm aware of what UndecidableInstances does.
But in this case, it's actually ensuring the soundness of the
computational aspect of functional dependencies, at least in the case
where said computation were fixed to incorporate the things type
families can do. Which would be useful, because fundeps don't interact
with GADTs and such correctly.
> The coverage condition is part of a pair of pair of sufficient (but
> not necessary) conditions that GHC applies to know that typechecking
> is decidable. It just says that if you have a dependency "a -> b",
> and you have type variables in b, then they should mention all the
> type variables in a. Thus, the following code is legal without
> UndecidableInstances:
>
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE FunctionalDependencies #-}
>
> class A a b | a -> b
> instance A [a] (Either String a)
In this instance, the second argument can be given as a function of the first:
f [a] = Either String a
> But the following program is not:
>
> class A a b | a -> b
> instance A a (Either String b)
In this instance, it cannot.
> No, that's not right. Even with UndecidableInstances, you cannot
> define conflicting instances for functional dependencies. Moreover,
> just because the GHC's particular typechecker heuristics don't
> guarantee the above code is decidable doesn't mean it isn't decidable.
You certainly can define conflicting instances if 'a -> b' is supposed
to denote a functional dependency between a and b, and not just a
clever set of rules for selecting instances.
> I think you are thinking of UndecidableInstances in the wrong way.
> For instance, the following code does not require
> UndecidableInstances, but has polymorphic type variables on the
> right-hand side of a functional dependency, which seems to be what you
> object to:
>
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE FunctionalDependencies #-}
>
> class C a b | a -> b where
> foo :: a -> b
>
> instance C (Either a b) (Maybe b) where
> foo _ = Nothing
>
> bar :: Maybe Int
> bar = foo (Left "x")
>
> baz :: Maybe Char
> baz = foo (Left "x")
This is another case where the second argument is a function of the first:
f (Either a b) = Maybe b
bar uses the induced instance C (Either String Int) (Maybe Int), and
baz uses the induced instance C (Either String Char) (Maybe Char).
> Remember, FunctionalDependencies are all about determining which
> instance you select. The functional dependency "class C a b | a -> b"
> says that for a given type a, you can decide which instance of C
> (i.e., which particular function foo) to invoke without regard to the
> type b.
Why are they called "functional dependencies" with "a -> b" presumably
being read "b functionally depends on a" if there is no actual
requirement for b to be a function of a?
> It specifically does *not* say whether or not type b has to
> be grounded, or whether it may include free type variables, including
> just being a type variable if you enable FlexibleInstances:
I don't personally count free type metavariables as Haskell types.
They are artifacts of the inference algorithm. Int is a type, and
(forall a. a) is a type. But a metavariable 'b' is just standing in
for a type until we can figure out what actual Haskell type it should
be. Haskell muddies this distinction by only allowing prenex
quantification, and writing 'a -> b' instead of 'forall a b. a -> b',
but the distinction is actually important, if you ask me.
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE FunctionalDependencies #-}
> {-# LANGUAGE FlexibleInstances #-}
>
> class C a b | a -> b where
> foo :: a -> b
>
> instance C (Either a b) b where -- no UndecidableInstances needed
> foo _ = undefined
This is yet another example where the second parameter is actually a
function of the first.
> Again, unique but not grounded. Either Maybe c or "forall c" is a
> perfectly valid unique type, though it's not grounded. People do
> weird type-level computations with fundeps using types that aren't
> forall c. (The compiler will fail if you additionally have an
> instance with forall c.)
(forall c. Either Maybe c) is a valid type. "forall c" on its own is
not a type at all, it's a syntax error. And a metavariable 'c' is
something that exists during inference but not in the type system
proper.
> I think the reason you have the right-hand side is so you can
> say things like "| a -> b, b -> a".
The reason they have a right hand side is that these are
specifications of *functional dependencies* between the parameters.
That is, in the above, b is a function of a, and a is a function of b.
Or, in my example, c is a function of a and b, but not d.
> But anyway, even if you think of fundeps as primarily being functions
> on types, those functions can be polymorphic. Just as it's not
> super-useful to have functions like "f :: String -> a" other than
> error, people often don't do this for fundeps. But relaxing the
> coverage condition still doesn't lead to conflicting functional
> dependencies. No combination of flags to GHC will allow you to have
> conflicting functional dependencies.
'instance C a b' is not specifying a "polymorphic" function between
the two parameters. It is specifying that there is a non-functional
relation between them. The relation C holds for all a and b. So, C Int
Int holds, as does C Int Char and C Char Int. So C is manifestly *not
a function*. Yet we could have declared that its second argument is
functionally dependent on its first, meaning that C should be a
functional relation. And with undecidable instances, this declaration
will still go through fine. So we have declared C to be functional,
but it is not.
If we want to talk about ground variables and such, let me ask this:
in Mercury, if I declared that f were a *function*, would 'f(5,X)'
(assuming I've got the syntax right) allow X to be an unground logic
variable that could unify with anything? I suspect the answer is "no."
If this is really about rules for selecting instances unambiguously
without any regard to whether some parameters are actually functions
of other parameters, then the name "functional dependencies" is pretty
poor.
> There have been some questions about soundness and fundeps. Don't worry. I'm certain
> GHC's implementation fundeps is sound.
I know the actual implementation is, too. But it's because of the
limited way in which fundeps are used. If I'm not mistaken, if they
were modified to interact with local constraints more like type
families (that is, correctly :)), then soundness would be a concern
with these examples.
> Dan asks why
> instance (r~False) => Eq j k r
> could possibly differ from
> instance Eq j k False
I understand why the instance resolution causes these to be different
in Haskell. I think the first one is a bad definition by the same
criteria (although it is in practice correct due to the constraint),
but UndecidableInstances turns off the check that would invalidate it.
-- Dan
More information about the Haskell-prime
mailing list