TypeFamilies vs. FunctionalDependencies & type-level recursion
dan.doel at gmail.com
Tue Jun 14 21:09:02 CEST 2011
On Tue, Jun 14, 2011 at 1:19 PM,
<dm-list-haskell-prime at scs.stanford.edu> wrote:
> No, these are not equivalent. The first one "TypeEq a b c" is just
> declaring an instance that works "forall c". The second is declaring
> multiple instances, which, if there were class methods, could have
> different code. The second one is illegal, because given just the
> first two types, a and b, you cannot tell which instance to pick.
Then why am I not allowed to write:
class C a b | a -> b
instance C T [a]
without undecidable instances? GHC actually complains in that case
that the coverage condition is violated. But it is a single well
specified instance that works for all a.
The answer is that such an instance actually violates the functional
dependency, but UndecidableInstances just turns off the checks to make
sure that fundeps are actually functional. It's a, "trust me," switch
in this case (not just a, "my types might loop," switch).
So I guess HList will still work fine, and UndecidableInstances are
actually more evil than I'd previously thought (thanks for the
correction, Andrea :)).
> A functional dependency such as "| a b -> c d" just guarantees that a
> and b uniquely determine the instance. Hence, it is okay to have
> class methods that do not mention type variables c and d, because the
> compiler will still know which instance to pick.
It specifies that a and b uniquely determine c and d, so the choice of
instances is unambiguous based only on a and b. This is the basis for
type level computation that people do with fundeps, because a fundep
'a b -> c' allows one to compute a unique c for each pair of types.
If it were just about variable sets determining the instance, then we
could just list those. But I can write:
class C a b c d | a b -> c
And it will actually be a, b and d that determine the particular
instance, but just listing 'a b d', or using the fundep 'a b d -> c'
is wrong, because the fundep above specifies that there is a single
choice of c for each a and b. So we could have:
C Int Int Char Int
C Int Int Char Double
C Int Int Char Float
but trying to add:
C Int Int Int Char
to the first three would be an error, because the first two parameters
determine the third, rather than the first, second and fourth.
Being allowed to elide variables from the types of methods is one of
the uses of fundeps, and probably why they were introduced, but it is
not what fundeps mean.
> On the other hand, though the compiler won't accept it, you could at
> least theoretically allow code such as the following:
> instance C [Char] where
> type Foo [Char] = forall b. () => b
The fundep equivalent of this is not 'instance C [Char] b'. It is:
instance C [Char] (forall b. b)
except types like that aren't allowed in instances (for good reason in general).
The closest you could come to 'instance C T b' would be something like:
type instance F T = b
except that is probably interpreted by GHC as being (forall b. b).
More information about the Haskell-prime