Multiple implementations using relations
----------------------------------------
This is about multiple implementations of the same abstract data type.
I'll argue that relations are more appropriate than functions for
operating on these types.
We consider the usual example of complex numbers, which have both
polar and rectangular implementations. It seems natural to write
C = P + R
so let's do that. Then perhaps can we type a complex conjugate
function as
conjugate : C -> C
But this doesn't seem quite right. It's clear that the function
should be able to operate on either type, so the domain is right, but
the codomain seems funny. How do we know when it returns R and when
it returns P? Furthermore, how can we restrict this function to one
of these more specialized functions:
conjugateRR : R -> R
conjugatePP : P -> P
conjugateRP : R -> P
conjugatePR : P -> R
Again, there is no particular problem with the domain, but how do we
choose the codomain? The answer I'm suggesting is clear by now: use a
relation on C = R + P, rather than a function:
conjugate : C <-> C
Then conjugate(c1, c2) is true whenever c1 and c2 are conjugates,
regardless of their representation. The usual notion of restriction
on relations gives the four functions above.
Motivation
----------
Suppose a computational routine receives a function as argument. Not
only do we want to specialize the routine to the range of the
function, we also want to specialize the function to the domain on
which it is applied. For example, if we pass generic SIN to an
"integrate on R" routine, we want to use a specialized SIN on R.
Function generators
-------------------
Hence, we never pass a function to a routine, but a _function
generator_ that accepts a domain type and returns a range type and a
specialized function.
Function generators follow the general principle "first compute on
types, then on values." That is, we don't interleave the two.
Actually, suppose f is a function object. Then:
(object-type f) : domain_type -> range_type
(object-value f) : domain_type -> [procedure for f]
Function types
--------------
In this system, a function _type_ accepts a domain type and returns a
range type.
So the type of SIN is similar to SIN itself, except that it computes
over types, which are abstract values. That is,
(sin-type real-type) = real-type
(sin-type zero-type) = zero-type
(sin-type positive-real-type) = real-type
We could do better:
(sin-type real-type) = unit-interval-type
This notion is more flexible than the usual arrow types.
Also note that generic sin can compute over types as well as values.
So "sin" and "sin-type" could be identical. There would be a separate
"restrict generic" routine to extract specialized functions.
What base types to use?
-----------------------
We choose base types according to their utility for making more
efficient specialized functions.
-------------------------------------------------------------------
That's about it for the type system, but here are some notes on
various (supposedly) related topics.
Why arrow types are limited
---------------------------
We don't know the result type of a function until we know what
arguments it is applied to. For example, SIN can return complex, but
if we only apply it to zero, that hardly matters.
The usual "arrow types" are "one-point" approximations to the graph of
a function. For example, unary minus might have type R => R, but a
better approximation would be { neg -> pos, 0 -> 0, pos -> neg }. That
would be a "three-point" approximation.
The type
{ neg -> pos, 0 -> 0, pos -> neg }
is just like the product
(neg -> pos) * (0 -> 0) * (pos -> neg),
except for ordering, etc.
Sum types versus multiple implementations
-----------------------------------------
There is a slight difference between these ideas. First, let's
describe sum types. Suppose
Complex = Rectangular + Polar
Negate : Complex -> Complex
Negate then accepts either Rectangular or Polar, appropriately tagged,
and returns, at its discretion, either Rectangular or Polar.
Multiple implementations are slightly different. For any pair of
(in-type, out-type), we can make a function
Negate : in-type -> out-type.
Of course, some I/O pairs might not be available. Another way to say
it is that with sum types, we can control the input type but not the
output type. With multiple representations, we can control both.
Suppose we have the obvious four implementations of negate. Negate
isn't a function, since negate on R can return either R or P. But it
_is_ a relation; (negate r p) is true iff p represents the negation of
r. Then we can restrict both the domain and range to obtain a
function, that is, to extract a single implementation. The negate
relation would have the type:
{ (R -> R), (R -> P), (P -> R), (P -> P) }.
How to select implementations
-----------------------------
The type system described above uses "forward abstract interpretation"
combined with "explicit specialization". It's called "forward"
because types are determined by the inputs rather than the outputs.
It's "explicit" since we're manipulating the types explicitly rather
than saying "compile this code".
Unfortunately, I don't think forward analysis is sufficient for good
implementation selection (an example?). To do both forward and
backward, we could solve a constraint system with cost information,
which is roughly what we want.
Also, I don't see how to do that explicitly. So it looks like the
only technique is to generate a program representation using forward
analysis (using placeholders, like Andy did) and then analyze it
separately.
Of course, if we go this far, we could probably do the whole type
system implicitly. But now we're talking block compilation.
Mathematical type and implementation type
-----------------------------------------
I think Zippel's two types are less significant than they appear.
Certainly we want to distinguish different types of numbers at top
level. But suppose
Complex = Rectangular + Polar.
We have a choice of representation. We could say:
(COMPLEX-TAG (LEFT-TAG rectangular-rep)) and
(COMPLEX-TAG (RIGHT-TAG polar-rep))
or
(RECTANGULAR-TAG rectangular-rep)
(POLAR-TAG polar-rep).
The only difference is in the organization of the tag namespace.
Opacity is an orthogonal issue. It is easy enough to make either
representation appear as [COMPLEX-NUMBER xxx] and to limit the set of
allowed operations.
It seems that "mathematical type" versus "implementation type" is the
usual "abstract" versus "concrete" distinction, which is basically
about opacity.
Subtypes, coercions, and inheritance
------------------------------------
Are you thinking of managing subtypes and coercions explicitly?
I would imagine something like
(declare-subtype! x y coercion)
(subtype? x y)
(get-coercion x y).
I wouldn't use inheritance too much, since it inherits both type and
implementation. And what's worse, it builds subtype implementations
from supertype implementations. So if REAL is a subtype of COMPLEX,
it builds REAL implementations from COMPLEX implementations.
Polymorphism versus genericity
------------------------------
A generic function accepts arguments of several types. A polymorphic
function can be specialized on any of several types. If you like,
it's
(generic-function type argument) versus
((polymorphic-function type) argument).