Revising the Simple Type System

[jbs1]

migrated from Trac, where originally posted by lars_h on 30-May-2014 5:38pm

This is a proposal for a revised Simple Type System. The main innovation is to use regular word languages to describe the argument structures of application symbols, particularly those that are variadic. It also provides for symbols with multiple signatures (polymorphism).

The following uses ALL-UPPER-CASE for metasyntactic variables and Popcorn-ish cd.name identifiers for specific symbols. (Exactly how to phrase a formal specification of the following would need further thought.)

The main nonterminal in this grammar is TYPE. If you would annotate an object with a type, then this is primarily what you would want (but see also SIGNATURE further down).

TYPE = OMV
     | sts.mapsto(AWL,TYPE)
     | sts.binder(AWL,AWL,TYPE)
     | OTHER-CASES-OF-TYPE

An OMV is of course a named (probably abstract) type, like <OMV name="AbelianSemiGroup"/>. An AWL is an Argument Word Language, defined below; the cases of an sts.mapsto with more than two arguments are treated as a shorthand, so they would still work as in present STS. sts.binder is changed from constant to something sts.mapsto-like, as sketched in http://www.openmath.org/standard/sts.pdf but with separate declarations for bound variables, body, and result (in that order).

AWL = TYPE
    | sts.or(AWL,AWL,...)
    | sts.block(AWL,AWL,...)
    | sts.nary(AWL)

An AWL is basically a regular word language over the alphabet of all TYPEs (obviously not requiring said alphabet to be finite for that metaphor). If AWL seems like a weird term then maybe TEMPLATE could be an alternative, but I'll stick with AWL for now.

The new symbols sts.or and sts.block should be n-associative.^[#note1 1]^ sts.or is union of languages (like | in most regexp syntaxes), whereas sts.block is concatenation of languages (the vulgar interpretation would be as a regexp parenthesis). sts.nary is the Kleene star, because that's what it already is if you think about it. One could add some sts.optional and sts.oneormore (regexp ? and + respectively), since they're a bit awkward to express with sts.or and sts.block. The language of the length 0 word is of course sts.block() and the empty language is sts.or(), but I doubt the latter will ever be useful in this context.

Any sts.mapsto($x1,...,$xn,$y) is a shorthand for

   sts.mapsto(sts.block($x1,...,$xn),$y)

There is no similar shorthand for sts.binder. Instead I anticipate #136 in the above grammar.

Finally, we get down to the actual signatures.

SIGNATURE = TYPE
          | sts.or(TYPE,TYPE,...)
          | sts.error
          | sts.attribution

The point of or'ing here is purely to support polymorphic symbols. sts.error and sts.attribution appear here (rather than under TYPE) because the identifier of an OME or OMATP has to be a naked symbol.

Some examples:

Laplacian (from Davenport (2000), footnote 8)

sts.or(
  sts.mapsto( sts.mapsto($Vector,$Scalar), sts.mapsto($Vector,$Scalar) ),
  sts.mapsto( sts.mapsto($Vector,$Vector), sts.mapsto($Vector,$Vector) )
)

Universal quantifier (quant1.forall)

sts.binder(sts.nary(sts.Object),$Boolean,$Boolean)

Binding definite integral, curried (\int\colon (a,b) \mapsto \int_a^b)

sts.mapsto($Real,$Real,sts.binder($Real,$RealCompleteVector,$RealCompleteVector))

The elementary calculus definition of the simple definite integral requires the variable and the bounds to be real, but the value of the integrand and the value of the integral can belong to pretty much any real vector space as long as that is complete.

Lambda (fns1.lambda)

sts.binder(sts.nary(sts.Object),sts.Object,$Function)

This is not completely satisfactory, since one would like to be clear about the type of the $Function as well, but the problem is that

sts.binder(
   sts.nary(sts.Object),
   sts.Object,
   sts.mapsto(sts.nary(sts.Object),sts.Object)
)

would be wrong; it fails to express the restriction that both sts.nary(sts.Object) have to have the same number of repetitions. One could imagine some extension of the simple type system that allows expressing such restrictions, but I suspect it's not worth it; lambda is a rather special symbol.

On the other hand, there is — particularly in functional programming — a couple of concepts which would have similar links between bound variables and function type. In particular, there is is letrec, which would be something like

sts.binder(sts.block($Function,sts.nary(sts.Object)),sts.Object,$Function)

— the first bound variable is also what this binder returns. It might (as always) be argued that a letrec is unnecessary as separate symbol, since it can be defined using lambda and a fix-point combinator, but I'm not sure it is quite so simple. For one, the right way to define a fix-point combinator depends heavily on the evaluation strategy being employed (I seem to recall that what is right for standard order evaluation diverges horribly under normal order evaluation), whereas letrec is not so sensitive; OpenMath does not have a preferred evaluation order. Second, I seem to recall that one reason for introducing letrec (or some similar construct) is that it simplifies doing typed lambda calculus.

where clause (f(t) where t = g(x)), curried

sts.mapsto($Object,sts.binder($Object,$Object2,$Object2))

I'm a bit inclined to use the name erehw for such a symbol, since it has the parts in the opposite order of that in which they would appear in a colloquial where clause:

<OMBIND>
  <OMA>
    <OMS cd="lambdacalc1" name="erehw"/>
    g(x)
  </OMA>
  <OMBVAR> t </OMBVAR>
  f(t)
</OMBIND>

Of course, this is very close to the standard lambda, so the main point of defining such a symbol would probably be to simplify presenting it as a where clause (a situation similar to that of the Landauin^[#note2 2]^).

An interesting point in the signature as presented above is that it says that the two $Object and the two $Object2 repectively are of the same type, even though $Object and $Object2 need not have the same type. Just using sts.Object for all four would not convey this distinction.

This leads us to the matter of types-as-free-variables vs. types-as-constant-symbols. jhd has at some place remarked that this corresponds to the distinction between abstract and constructive types. I tend to agree, but feel that it could do with being explained more fully in the specification. In particular, I'm conflicted about the use of free'' variables. On one hand, this would mean that the same variable should mean the same thing in all signatures of a file, which seems good, but on the other hand it feels a bit odd to have them free variables. The variables are being used as "new constants distinct from all old values" rather than as plain variables. Of course, this is a common way to use variables (especially in things like Q[''x'',''y''] the ring of polynomials in ''x'' and ''y), but formally it tends to come out a bit strange.

Another matter is that even if one is mostly stating things in terms of abstract types (which is often what one wants to do), there are occasional cases of functions that need some argument to be in a very concrete set (e.g. the integers). I've seen cases where symbols for those sets are then used as TYPEs, e.g. group1.power could have the signature

sts.mapsto($Group,$GroupElement,setname1.Z,$GroupElement)

(turns out there is no entry for group1.power in group1.sts, although there is one in group1.ocd), however it would feel slightly more natural to me if there was an application symbol sts.elementof that turned an arbitrary set into the type "element of that set". Then one could express a type such as

sts.mapsto(
  sts.elementof({"A","B","C","D","E","F","G"}),
  sts.elementof(setname1.Z),
  $DynkinDiagram
)

for some function that produces a Dynkin diagram from the relevant letter and index.

[=#note1]^1^ Not included in the above is sts.nassoc, which is perhaps a bit ironic as I used n-associativity to characterise the two new symbols sts.or and sts.block, but I really don't see the extra claim it is making relative to sts.nary as fitting in with the basically syntactic nature of the type system. N-associativity should rather be expressed as an FMP, and I have an idea on how to do that, but I think I want to make that the topic of a paper for OM2014.

[=#note2]^2^ I thought the Landauin symbol had been put in a CD, but I don't see it in http://www.openmath.org/cdindex.html. In that case, I hope there's still time to rename it Landau_in.

[lars-hellstrom]

The formatting in one paragraph above got mangled in the conversion. Should rather be:

This leads us to the matter of types-as-free-variables vs. types-as-constant-symbols. @JamesHDavenport has at some place remarked that this corresponds to the distinction between abstract and constructive types. I tend to agree, but feel that it could do with being explained more fully in the specification. In particular, I'm conflicted about the use of free variables. On one hand, this would mean that the same variable should mean the same thing in all signatures of a file, which seems good, but on the other hand it feels a bit odd to have them free variables. The variables are being used as "new constants distinct from all old values" rather than as plain variables. Of course, this is a common way to use variables (especially in things like Q[x,y] the ring of polynomials in x and y), but formally it tends to come out a bit strange.

[kohlhase]

you can (and should) just do that by editing the issue description (the little pen in the upper right hand corner)

[lars-hellstrom]

@kohlhase No I can't, because github doesn't understand I created it.

[kohlhase]

actually, I think the reason is that you do not have write access. I have given that to you, please accept.

[kohlhase]

moved to OpenMath/OMSTD#39