Concrete Syntax Again

Arising from today’s headbanging session, we have another round of proposed concrete syntax evolution. Here’s the loose context-free approximation.

(Grammar grammar: angle brackets are the meta-brackets here; ? means ‘0 or 1’; * means ‘0 or more’; + means ‘1 or more’; ,* means ‘0 or more, comma-separated’ and similarly for + and for other separators.)

Expressions

\[
\begin{array}[t]{rl}
\textsc{Small} := & (\left< \textsc{Field}\right>^{;\ast}) \\
| & \textsc{Var} \\
| & \texttt{\_} \\
| & [\textsc{Text}] \medskip \\
\end{array}
\]

\[
\begin{array}[t]{rl}
\textsc{Field} := & \left< \_\right>^{?}\:\left< \textsc{Pat}\texttt{=>}\right>^{?}
\: \textsc{Term} \left< \texttt{:}\textsc{Term}\right>^{?} \\
\end{array}
\]

\[
\begin{array}[t]{rl}
\textsc{Term} := & \textsc{Small}^+ \\
| & \textsc{Bop}\: \textsc{Sig}\: \textsc{Rhs} \medskip \\
\end{array}
\]

\[
\begin{array}[t]{rl}
\textsc{Var} := &  \textsc{Id}\left< {{}^{\wedge}\textsc{Nat}}\right>^? \medskip \\
\end{array}
\]

\[
\begin{array}[t]{rl}
\textsc{Bop} := & \texttt{lam} \\
| & \texttt{all} \\
| & \texttt{ex} \\
\end{array}
\]

Remarks:

  • Tuples are bracketed vertical sequences.
  • Binders may take right-hand sides other than ‘⇒ blah’, so you can write little programs in them.
  • Variables carry an optional de Bruijn index, with x^n meaning ‘skip the most local n x’s and take the one before that’. This provides a way to reference a variable which has been shadowed.

Signatures

\[
\begin{array}[t]{rl}
\textsc{Sig} := & \textsc{Bind} \\
| & \textsc{Sig};\textsc{Sig} \\
| & \left\{\Rule{\textsc{Shadow}\: \textsc{Sig}}
{\textsc{Sig}}\right\} \\
| & [\textsc{Text}] \medskip \\
\end{array}
\]

\[
\begin{array}[t]{rl}
\textsc{Bind} := & \textsc{Pat}^{,\ast}\:
\left< {\texttt{:}\textsc{Term}}\right>^? \medskip \\
\end{array}
\]

\[
\begin{array}[t]{rl}
\textsc{Shadow} := & \left< {\{\textsc{Bind}^{;\ast}\}}\right>^? \medskip \\
\end{array}
\]

\[
\begin{array}[t]{rl}
\textsc{Pat} := & \textsc{Var}\:\textsc{Pat}^{\ast} \\
| & (\textsc{Pat}^{;\ast}) \\
| & \texttt{lam}\:\textsc{Sig}\:\texttt{=>}\:\textsc{Pat} \\
| & [\textsc{Text}] \medskip \\
\end{array}
\]

Remarks:

  • Bindings now allow higher-order patterns (most general, because of η-laws). This is handy for splitting up tuples, and especially handy for matching a function to tuples as a tuple of functions. Free variables in patterns are explicit binding occurrences and guarantee to shadow more global variables of the same name.
  • The ‘shadow’ contains the implicit binders for variables used without declaration and then generalised. The editor might only show those bindings in the shadow which are required to, er, shadow variables which would otherwise be captured by a more global variable of the same name. However, such an editor might save the whole of the shadow explicitly in source files, to maintain their stability with respect to thinning even while it isn’t watching.

Programs

\[
\begin{array}[t]{rl}
\textsc{Rhs} := & \texttt{=>}\: \textsc{Term} \\
| & \texttt{<=}\: \textsc{Term}\:\textsc{Rhs} \\
| & \texttt{||}\: \left<\left<\textsc{Id}\texttt{:}\right>^?\textsc{Pat}\texttt{=}\right>^?\textsc{Term}\:\textsc{Rhs} \\
| & \{\textsc{Prog}^{;\ast}\} \\
| & [\textsc{Text}] \medskip \\
\end{array}
\]

\[
\begin{array}[t]{rl}
\textsc{Prog} := & \textsc{Lhs}\:\textsc{Rhs}\:\left< {\texttt{where}\:\textsc{Shadow}}\right>^? \\
| & [\textsc{Text}]  \medskip \\
\end{array}
\]

\[
\begin{array}[t]{rl}
\textsc{Lhs} := & \left< {\textsc{Bop}}\right>^?\:\textsc{Small}^{\ast}
\:\left< \texttt{|}\:\textsc{Term}\right>^{\ast} \medskip \\
\end{array}
\]

Remarks:

  • Whilst there is no good reason ever to reduce a programming problem trivially to the identical subproblem, there is no good reason to forbid it.
  • Adopting the convention that the scope of the left hand side extends to the whole of the right hand side, including subprograms, means that it makes sense to stack up ⇐s and ||s, with the tail refining every subproblem of the head.
  • The optional binding operator in left-hand sides is a context-free fudge of the real situation. An lhs of a let will be a call to the function being defined. An lhs for a binder being given by cases carries the bop. As in
    
\[\AR{
\exists \vx\hb\vS\TC{+}\vT\:\BY\:\RW{case}\:\vx \\
\quad \exists\:(\DC{inl}\:\vs)\:\TO\:\vP\:\vs \\
\quad \exists\:(\DC{inr}\:\vt)\:\TO\:\vQ\:\vt
}\]
  • The optional pattern in ‘with’ names (pieces of) the abstracted computation; the optional identifier names the proof that the pattern is propositionally equal to the abstracted computation.

Top Level

\[
\begin{array}[t]{rl}
\textsc{Decl} := & \texttt{data}\:\textsc{Sig}\:\texttt{where}\:\textsc{Sig} \\
| & \texttt{let}\:\textsc{Sig};\:\textsc{Prog} \\
| & [\textsc{Text}] \medskip \\
\end{array}
\]

\[
\begin{array}[t]{rl}
\textsc{Source} := & \begin{array}[t]{l}
\hline
\left< \begin{array}[t]{l}
\textsc{Decl}\\
\hline
\end{array}\right>^{;\ast} \\
\end{array}
\end{array}
\]

Remarks:

  • I’ve quietly dropped inspect. This is perhaps a bit premature, but I’m hoping the same functionality (and more) will be delivered by scoped comments.
  • Still missing from this picture is any notion of module or package. More anon.

More Remarks

This suggestion represents an alternative to the ‘sombrero’ suggestion. Recall the problem: prevent capture of implicitly bound variables in signatures and left hand sides; the sombrero plan was to allow a special mark on the first occurrence of a variable to be considered fresh, if there was any chance of mistaken identity; this plan resolves ambiguity in implicit binding by explicit binding, providing a place for this to happen in programs as well as signatures. The two are not mutually exclusive, and I don’t know what’s for the best. I imagine some people might have strong opinions, eg, that this isn’t a problem worth solving. Please respond to this issue, sooner rather than later.

My current vacillation tends to implementing sombrero in the first instance—it’s an unimaginative hack. Paradoxically, this is because where clauses should serve other purposes too, so we need to think more before we introduce them…

One Response to “Concrete Syntax Again”

  1. Conor Says:

    http://www.e-pig.org/epilogue/current/src/Concrete.lhs contains the new parser, which is quite like the old one… Scope resolution next.

Leave a Reply