Re: semantical annotations

  First, there was a typo in the polynomial in my last example. It
  should be X^^3+2*X^^2+2, not X^^^^3+2*X^^^^3+2, in Axiom syntax (with
  a corrected exponent).

  Within a given type, we would expect all non-type objects to be
  represented in HTML math. If you look closely, you'll see that a
  type name is really just a function application, where other types
  can be arguments. So specifying a type is no more difficult than
  giving any other application form. The problem then is just one
  of where one puts it as annotation. To continue with the Axiom
  example, you would say
     x @ T
  to indicate that the expression x should be interpreted as having
  type T. This is no more difficult that parsing any other infix function
  application. Some other syntax in HTML math is acceptable, of course.
  [I don't remember if '@' is used.]

  If we had something similar, non-type-based systems would be free
  to disregard the type and process the expression x. (This could cause
  semantic errors, but no fewer than omitting all type information.)

  Note that I am not recommending a universal definition of all important
  types. I'm just talking syntax for allowing consenting apps and browsers
  to transmit the information. Just as not all specialized CAS can handle
  finite field extensions, not all will be able to handle types. However I
  would expect that most of the big name CAS can agree what
  ArbitraryPrecisionInteger is if they see it.

  Bob