TypeFamilies vs. FunctionalDependencies & type-level recursion

[oleg at okmij.org]

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.


About dynamic loading [perhaps this should be moved in a separate
thread?]

> 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.