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.
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
