akuklev: (Свечка и валокардин)
Extensible complex expression syntax [AEK 01627-0]

I'm deeply in love with syntactical strength of Agda, the most syntactically advanced mature programming language today:

– In Agda (almost) everything without spaces is an identifier, so multi-word identifiers can we written using nice CSS-ish style (e.g. vertical-align, status-line). Dashes look very much better than underscores or lowerCamelCase.
⇒ No need for ugly identifiers

– In Agda you can use the whole strength of unicode.
⇒ No need for ugly operators

— Infix operators are handled flexibly, mixfix operators (including, say, Oxford brackets) are supported.
⇒ Appropriate for complex mathematical expressions

There are, however, few weaknesses:

– Infix operators can be set to be left- or right-associative, there is no keyword for left or right accumulative operators, thus stacked equalities (a = b = c) and inequalities (a < b < d) are not supported. Accumulative operators can be easily introduced into Agda.

– Multiplication by juxtaposition is also not supported. For the case the first operand is an integer number this can be easily addressed by slight modification of lexer rules, for all other cases one can use whitespaces instead: [a + b]^2 = a^2 + 2a b + b^2. By introducing a rendering rule that single-letter identifiers are rendered in italics (as in TeX) and whitespaces between them omited, we can get the best of both worlds.

– No whitespaces in names of mixfix operators are allowed, parsing of expressions with mixfix operators by readers' eyes can be nontrivial. There is an unused resource that can be used to remedy this issue: UPPERCASE WORDS. With an exception to single-letter uppercase identifiers (that are generally used for matrix-valued, operator-valued and set-valued variables in mathematics and programming) UPPERCASE WORDS are non normally used in identifier names in Agda. So we could declare that they are reserved for mixfix operators only. The distinction between UPPERCASE WORDS and normal identifiers is unambiguous already on lexing stage, so we can allow for whitespaces in mixfix operators. Uppercase words should be rendered as bold lowercase ones, for it's much more optically pleasing. In both cases, the readers' eye parsing becomes easier:
  IF condition THEN something ELSE something-else

  if condition then something else something-else
There is also a very natural usecase for CamelCase: CamelCase should be used for labels (equation labels, theorem names, labels of sections in structured documents, block labels in code) and other entities with identity not amounting to the content: symbols (elements of enum), constructor names, names of opaque objects and members: modules and library types, type members that should be path-dependent (I really want to add this killer feature to Agda). CamelCase identifiers should be rendered bold on all occasions except at their definition point.

I would additionally propose to use square brackets [] for grouping and and parentheses for type hints and other sort of hints, for it's closer to written english and optically more appealing. With these addenda we can write statements in a very literate fashion:
Theorem CayleyThm:
  for all G (Group) [there is S (Set) such that [G ≤ S!]]

Proof CayleyPrf1 (CayleyThm):
  Let g (G):

This approach (in slightly different form) was developed mainly by Alexander Temerev around summer 2007, we were developing the our own programming language back then.

December 2016

456789 10


RSS Atom

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 21st, 2017 03:47 pm
Powered by Dreamwidth Studios