See Guy Steele's slides for what I refer to by "Computer Science Metanotation", specifically the bits about BNF.

I often make use of the BNF syntax observed there, as a substitute for algebraic data types in functional programming languages. Alas, it loses quite drastically in appeal as soon as "fields" of function types are involved:

$$ \begin{array}{rrcl} \text{Naturals} & n & ∈ & \mathbb{N} \\ \text{NatLists} & l & ::= & [] \mid n :: l \\ \text{FunPair, v1} & p & ::= & (\mathbb{N} \to l) \sim (l \to \mathbb{N}) \\ \text{FunPair, v2} & p & ::= & f \sim b \\ \text{NatToList, v2} & f & ∈ & \mathbb{N} \to l \\ \text{ListToNat, v2} & b & ∈ & l \to \mathbb{N} \\ \text{FunPair, v3} & p & ::= & (f ∈ \mathbb{N} \to l) \sim (b ∈ l \to \mathbb{N}) \\ \end{array} $$

This typically means the following:

  • Meta variables such as $n$, $l$, $p$, $b$ and $f$ range over distinct "syntactic categories".
  • There are two kinds of definitions of these syntactic categories, depending on the "defining operator" used:
    1. When the defining operator is ∈, it has the usual meaning, for example that $n$ should range over elements of ℕ.
    2. The defining operator ::= is used to define inductive data types. Its RHS is to be interpreted as different productions of the meta variable on the LHS, acting like a non-terminal. This defines a context-free grammar deriving finite, inductive data elements that the meta variable on the LHS ranges over, along with the particular syntax those elements should have. A typical example in type theory is type contexts $Γ ::= ε \mid Γ, x:τ$. Here, we have $l ::= [] | n :: l$, generating as elements of $l$ all the finite lists over natural numbers such as the empty list $[]$, the 3 element list $3 :: 4 :: 5 :: []$ and so on.

Having explained NatList above, what I want FunPair to model is a forward-backward function pair with special syntax $f \sim b$, such that $f$ is a function from ℕ to NatLists and $b$ a function from NatLists to ℕ. Whether and how we can achieve a proper definition of $p$ with ::= is the subject of this post; hence there are four different versions of FunPair that I want to discuss.

A few things:

  • Embedding "primitive"/"built-in"/"ground" types such as the naturals is quite painless, although the difference in meaning of what comes right of the defining operators ∈/::= is a bit strange
  • The BNF definition of NatLists is rather neat. The equivalent in "pure math" would be quite uncomfortable, relying on a least fixpoint of some functional to be defined as a function or inference rule system
  • It is absolutely painful to try to make FunPair work.
    1. v1 doesn't know a meta variable/"non-terminal" that ranges over $\mathbb{N} \to l$ and $l \to \mathbb{N}$, hence it simply lists the type that meta variable would range over. But the range of that function type is an "anonymous" inductive type again (meaning we can refer to it by its meta variable $l$, but don't know the name of what $l$ ranges over), so we suddenly have a meta variable to the left or right of the function type constructor. Urgh!!
    2. v2 tries to improve a bit by giving a meta variable $f$ to the (still strange) type $\mathbb{N} \to l$ (likewise for $b$), at the expense of coming up with a dull name ("NatToList") and listing length.
    3. v3 tries a bit of a combination. It acknowledges that a meta variable must appear in the "production" but also tries to declare $f$ and $b$ inline. The type of $f$ and $b$ are still strange.

Here's an attempt that combines v3 with the (also common) convention that every meta variable needs to have an associated named type

$$ \begin{array}{rrclcl} \text{Naturals} & n & ∈ & \mathbb{N} & & \\ \text{NatLists} & l & ∈ & L & ::= & [] \mid n :: l \\ \text{FunPair, v4} & p & ∈ & A & ::= & (f ∈ \mathbb{N} \to L) \sim (b ∈ L \to \mathbb{N}) \\ \end{array} $$

This is quite a bit better, but the notation $(f ∈ \mathbb{N} \to L) \sim (b ∈ L \to \mathbb{N})$ is still somewhat painful.

These issues are not specific to function types (although they are the most common), but also come up with quite a lot of other "pure math" type constructors.

What do you think? More concretely, my questions are:

  1. Has this problem come to your attention in practice, too?
  2. How did you resolve the "need a meta variable for a pure math type" issue?
  3. How did you resolve the "need a type for an anonymous inductive type" issue?
  4. Would you say it makes sense to try to evolve CSM's BNF notation or should we acknowledge its limits and try establishing a different notation to define the "data types" of your domain?
  • $\begingroup$ I don't understand what you're trying to represent with ArrayRef, and I'm not familiar with the syntax you're using. What do $n,i,l$ represent? $\endgroup$
    – D.W.
    Commented Mar 28, 2023 at 21:16
  • $\begingroup$ I edited the example to use a data type FunPair that is perhaps a bit more meaningful. The syntax should be somewhat familiar to someone reading papers about programming language design; it's quite prevalent in POPL papers, for example (Principles of Programming Languages). $\endgroup$ Commented Mar 29, 2023 at 8:08
  • $\begingroup$ I don't understand what FunPair is supposed to mean. Can you provide an explanation of what FunPair is alluding to, and what the letters $f,l,b$ represent? $\endgroup$
    – D.W.
    Commented Mar 29, 2023 at 8:32
  • $\begingroup$ I had another try. Read "This typically means the following ..." $\endgroup$ Commented Mar 30, 2023 at 8:24


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.