(*
 * Lots of things going on here.  Let's see if we can make them all work.
 *)
object Object;
object SummableList = SummableObject*;
object SummableObject < Object (**)=  integer(**);
    (*
     * Want the previous def to be simply
     *
     *     object SummableObject is Object.
     *
     * If it is, we'll have to extend type checking semantics something like
     * this:
     *
     *     If compat is otherwise going to fail, we look to see if there's an
     *     axiom defined for the name or any direct derivation or parent of the
     *     name, and if so if the axiom requires a certain type, and if that
     *     type is compat with what we're looking for, then we're good.  This
     *     is pretty heady territory here and we need to tread quite carefully.
     *
     *)
axiom Summable = forall (so:SummableObject) IsNumeric(so);

(*
 * Note that we might be able to do without the whole axiom business, at least
 * in the realm of type checking, with the following alternative definition:
 *
 *     object SummableObject is real or integer;
 *
 * and then using multiple inheritance to allow otherwise normal objects to
 * inherit from SummableObject so they can be members of a summable list.
 *
 * It's a bit murky, but I'm getting a feeling that the Java interface biznis
 * is in fact a way (probably weak) of getting OBJ-like theory/view behavior.
 * This certainly requires more thought.
 *
 * OK, here's a bit more thought.  I'm uneasy with the above statement
 *
 *     "use multiple inheritance ... so they can be members of a summable list"
 *
 * The unease is that it puts the burden summable listness on the list elements
 * rather than on the list itself.  I believe we've seen this kind of thing
 * plenty in our various dealings with generic structures.  This may be one of
 * the (fundamental) weakness of using Java-like 'type Object + multiple
 * inheritance' instead of the ML-like 'type vars and axioms'.
 *
 *)
function SumList(sl:SummableList)->real =
    if sl = nil
    then 0
    else sl[1] + SumList(sl[2:#sl]);
function IsNumeric(o:Object)->boolean =
    (typeof(o) = "integer") or (typeof(o) = "real");
function typeof(o:Object)->Type;
object Type = Tuple or Union or List or string;
object Tuple = TupleTag and Type*;
object Union = UnionTag and Type*;
object List = ListTag and Type*;
object TupleTag;
object UnionTag;
object ListTag;