# TypeFamilies vs. FunctionalDependencies & type-level recursion

oleg at okmij.org oleg at okmij.org
Tue Jul 5 06:47:26 CEST 2011

Sorry for the late reply.

> GHC does not accept the following program:
>   {-# LANGUAGE TypeFamilies #-}
>   x :: ()
>   x = const () (eq a b)
>       where
>         a :: S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(Z)))))))))))))))))))))
>         a = undefined
>         b :: S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(Z)))))))))))))))))))))
>         b = undefined
>         eq :: a -> b -> NatEq a b
>         eq _ _ = undefined
>
> Notice that there are no undecidable instances required to compile
> this function (or the portions of your TTypeable that this function
> depends on).  Yet GHC is still limiting my context stack (to 21 by
> default).  Obviously any kind of unicode encoding of type names is
> going to run into the same sort of problem.

I would call this a bug, a recent one. Old versions of GHC (before
6.10, I think) imposed no context stack restrictions on programs with
decidable instances. Such a restriction is a recent addition (perhaps
introduced as a safe-guard since it was discovered that the old
versions of GHC did not properly implement the coverage condition). I
would recommend to file this as a bug, including the sample code
above. Your old message argues well why this new behavior should be
considered as a bug.

> But now the comparison of types is depending on this context stack and
> likely worsening the problem.

I agree that dependence on the arbitrary limit is unsatisfactory. That
is why I was hoping that Nat kinds will eventually make their way into
GHC (there are many arguments for their inclusion, and some people are
reportedly have been working on them).

> Finally, I still think most of the "magic" in everything we've been
> talking about boils down to being able to have a type variable that
> can take on any type *except* a certain handful.  This would allow us
> to avoid overlapping instances of both classes and type families,
> would allow us to define TypeEq, etc.  Moreover, it would be a more
> direct expression of what programmers intend, and so make code easier
> to read.  Such a constraint cannot be part of the context, because

Alas, such type variables' with inequality constraints are quite
complex, and the consequences of their introduction are murky. Let me
illustrate. First of all, the constraint /~ (to be used as t1
/~ Int) doesn't help to define TypeEq, etc. because constraints are
not used when selecting an instance. Instances are selected only by
matching a type to the instance head. Instance selection based on
constraints is quite a change in the type checker, and is unlikely to
be implemented.

Let us see how the selection based on mismatch could be implemented.  To
recall, the constraint "t1 ~ t2" means that there exists a
substitution on free type variables such that its application to t1
and t2 makes the types identical. In symbols,
\exists\sigma. t1\sigma = t2\sigma
We call the type t matches the instance whose head is th if
\exists\sigma. th\sigma = t

Now, we wish to define selection of an instance based on
dis-equality. We may say, for example, that the instance with the head
th is selected for type t if
\not\exists\sigma. th\sigma = t
In other words, we try to match t against th. On mismatch, we
select the instance. Let us attempt to define TypeEq

class TypeEq a b c | a b -> c
instance TypeEq x x True
instance TypeEq x (NOT x) False

and resolve (TypeEq Int Bool x). We start with Bool: Bool matches x,
so the second instance cannot be selected. The first instance can't be
selected either. Thus, we fail. One may say: we should have started by
matching Int first, which would instantiate x. Matching Bool against
so instantiated x will fail, and the second instance will be
selected. The dependence on the order of matching leaves a bad
taste. It is not clear that there is always some order; it is not
clear how difficult it is to find one. I submit that introducing
disequality selection is quite a subtle matter.  The TTypeable approach
was designed to avoid large changes in the type checker.

If you attend the Haskell implementors workshop, you might wish to
consider giving a talk about overlapping instances and the ways to get
around them or implement properly.

> I wish I knew ML better, but from looking at that paper, I can't
> figure out the key piece of information, which is how to detect
> overlapping type instance declarations.  (Does ML even have something
> equivalent?)

ML does not have type-classes; they can easily be emulated via dictionary
passing. Also, local open (recently introduced in OCaml) suffices
quite frequently, as it turns out.

I admit though I don't fully understand the problem:

> In the absence of type families, I'm okay using something like
> haskell-plugins that returns Dynamic.  ...
> With type families, I'm at a loss to figure out how this could even
> work.  You would need to know have a runtime representation of every
> type family that's ever been instantiated, and you would need to check

Type instance selection (including type family applications) are all
performed at compile time. At run-time, when a plug-in is loaded, no
instance selection is performed. If you wish to adjust the interfaces
of the plug-in based on the host environment, you have to program this
directly (by passing dictionaries explicitly). This is not very
difficult. Incidentally, several approaches to typed compilation'
(or, de-serialization of typed code) are described at

http://okmij.org/ftp/tagless-final/tagless-typed.html#typed-compilation

illustrating how to implement a simple type-checker, to run alongside
the serializer.