[bitc-dev] Possible solution for type functions

[Jonathan S. Shapiro]

I'm depressingly certain that I am re-inventing constructor classes here,
but here goes...

Wren has suggested moving to a type system in which we can have functions at
the type level. That might be the right thing to do, and I'm going to look
at it, but it makes me a bit nervous. What follows is my path to an
alternate solution that may or may not work.

First, observe that the problem with type functions is that the relation is
not articulated. The issue I anticipate in going to type-level functions as
Wren suggests is that they need to be partial. Three-type, four-function
arithmetic, for example, is defined only over certain type triples. If so,
then we're not just talking about functions at the type level; we're talking
about dependent type-level functions or match-type.

It then occurred to me that we already *have* a mechanism for specifying
partial (that is: overloaded) functions: type classes. Further, we are
already contemplating type classes as first-class types. Finally, Wren
points out that when type functions satisfy certain constructive properties,
they are safe.

So what about if we replace functional dependencies with constructor
classes, such that we can say:

  typeclass ThreeArith<'d<'a,'b,'c>, 'a, 'b, 'c> {
    + : fn ('a, 'b) -> 'c
    -  : fn ('a, 'b) -> 'c
    ...
  }

where we require at type class instance constructions that a suitable
ternary constructor be supplied matching 'd<'a, 'b, 'c> and thereby
constraining 'a, 'b, 'c into a known structural relationship.

The first tricky bit is that we also allow 'd<'a, 'b, 'c> to be a
*closed*type class (that is: one whose legal bindings of 'a, 'b, 'c
are exhaustively
enumerated).

The second tricky bit is that we can allow instances for different
parametric instantiations of ThreeArith to overload the relevant operators.
So basically, if you are willing to specify the legal overloading
relationships, you can extend the operators.

Of course, this is type-level functions in disguise, since type constructors
can be viewed as structurally constrained type-level functions. By naming
the relevant type-level function explicitly, and making it part of the type
of the concrete type class (the term "instance" is becoming depressingly
overloaded here, isn't it?), it would appear that we dodge the soundness
problems of anonymous fundeps. Further, we leave ourselves syntactically in
a position where future extension to type-level functions is
straightforward.


Wren: I realize that the sketch above is far from a soundness proof, but it
smells to me like:

   1. It resolves the underlying fundep problem by making the type-level
   function explicit and checkable for consistency,
   2. Preserves the ability to do the safe parts of what fundeps permitted,
   and
   3. Leaves open the possibility of more general type-level functions for
   the future...
   4. without exceeding the space of what can be structurally inferred.

Does that seem credible to you? For example, can we reconstruct Simon's
unsoundness example in this re-framing?

This doesn't resolve the colliding instances problem - if anything it makes
it worse - but assume for the sake of discussion that there is some
disambiguation rule for instances.


shap
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.coyotos.org/pipermail/bitc-dev/attachments/20100803/d3f726e7/attachment.html