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