I am *finally* coming to understand (I think) something that Mark Jones
tried to tell me years ago: type class instances are inappropriate when it
might make sense to have more than one instance binding for a given [set
of] type[s]. Not his words precisely, but I think I got the sense of it
right.

The reason this confused me for so long is that we see this abuse all the
time in Haskell programs. Because the abuse has become so conventional, the
novice programmer (including myself) is led to the belief that this is the
"proper" way to do things. It seems to me that the syntactical design of
the language does little to discourage either the confusion or the abuse.

Anecdotally confirming this: type classes in BitC that live in the preamble
work very well. They work because (a) being in scope, they cannot be
overridden, and (b) being in scope, they have a locally visible resolution
in any unit of compilation. Or in some cases they work because the type
classes are "closed". In a few others, they work because the type classes
are "quasi-closed", meaning that the instances are generated by the
compiler. HasField is an example of a quasi-closed type class in BitC.

I continue to be bothered by the interaction between type classes,
inference, and genericity. At this point, I am *completely* convinced that
something like:

(Ord 'a) => BTree 'a


is a type that we should never see. We shouldn't see this because a BTree
should not be defined over a particular universally bound ordering, but
rather over any valid, non-overlapping ordering. If that is so, then the
right typing is something like:

BTreeMaker (OrderingFor 'a) -> BTree 'a


The reason that we are even tempted to reach for type classes here is in
two parts:

1. We tend to naively write the implementation of BTreeMaker using
unqualified operators (like '<'). This induces the compiler to infer that a
type class is required.
2. Inlining: a type class instance is a compile time constant, where a
parameter may be a run-time value.

The first is programmer error. The second reflects the fact that the type
system doesn't let us say what we want. That is, we would like to have a
type that is more like:

BTreeMaker inline OrderingFor 'a -> BTree 'a


where "inline" should be read to mean that "everything required to
partially evaluate the ordering parameter away at compile time is lexically
known at the point of instantiation".

Note: I do *not* intend that OrderingFor is a type class here, because it
is useful if OrderingFor can contain things other than method signatures,
notably type definitions and constant bindings. We can, however, logically
extend the type class notion to incorporate these. At that point, we
*could* take
the view that something like (Ord 'a) can appear either in constraint
position or in the position of a type. In constraint position it is a type
class constraint. In type position it specifies the type of a
compile-time-constant parameter (in which case the use of "inline" here is
unnecessary).

If this view is adopted, then I think that the current mechanism for
anonymous type class instances becomes ill-conceived. Anonymous instances
(which is to say: inferred operator bindings) should always bind the
"natural" definition of the operator, and the specification of what
constitutes a "natural" definition is up to the party defining the type. At
that point, I'd like to re-arrange the naming of the keywords to make it
more strongly clear that we are engaged in default bindings of operator
classes, and adjust the syntax accordingly, but I think that the "hack"
rule requiring that user-defined default instances must be defined in
certain units of compilation becomes tolerable.  All non-default type class
instances are named, and are bound in the usual lexical namespace. The
default binding should probably also be named.

In any case, my feeling is that introducing a notion of
compile-time-constant definitions into the language pragmatically resolves
a lot of the things that were driving me crazy. Partly by solving one of
the problems that I was struggling with, and partly by making the
define-in-same-module rule tolerable.


Jonathan
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to