# Progress Update (July 24, 2020)

As part of working with the garage door up, I've promised to share what I've been working on. I last updated on June 23. Unfortunately, progress has been limited, primarily since Tessa and I went on a half-vacation / half-working trip, which spanned most of two weeks. Then, I got back and started engaging with buying a house, so I've been a bit distracted.

## What's in a Term?

Despite that, I did manage to get substantial work done on a large-ish task, refactoring the structure of terms to be a bit more general. I haven't quite decided whether this is a good idea or not (leaning yes), hopefully this post helps to clarify my thoughts.

The core of the change is this diff in AbstractSyntax.mli:

``````--- a/src/AbstractSyntax.mli
+++ b/src/AbstractSyntax.mli
@@ -14,21 +14,18 @@ type sort =
| SortAp of sort_name * sort list (** A higher-kinded sort can be applied *)
| SortVar of string

+(** A sort can be starred to indicate it's repeated, or not. *)
+type starred = Starred | Unstarred
+
+(** Represents a place where a sort can go in a valence. *)
+type sort_slot = sort * starred
+
(** A valence represents the sort of an argument (to an operator), as well as the number
and sorts of the variables bound within it *)
-type valence =
-  | FixedValence of sort list * sort (** A fixed valence is known a priori *)
-  | VariableValence of sort * sort
-      (** A variable valence binds a number of variables not known a priori. All must be
-          of the same sort. *)
+type valence = Valence of sort_slot list * sort_slot

(** An arity specifies the arguments to an operator *)
-type arity =
-  | FixedArity of valence list
-  (** A fixed arity operator always has the same number of children *)
-  | VariableArity of sort
-  (** A variable arity operator has a variable number of children (all of the same
-      sort (non-binding valence)) *)
+type arity = valence list

type operator_def = OperatorDef of string * arity
(** An operator is defined by its tag and arity *)
``````

Note that the resulting code is simpler than before. We're generalizing two things here, which I'll show by example.

### The old way

First, let's talk about the old way of doing things. It was the case that you had two choices when it comes to valence: fixed or variable valence.

``````example :=
| fixed(a. b. a)  // fixed valence
| variable(a*. a) // variable valence
``````

An operator with fixed valence always binds the same number of variables, for example `fixed(a. b. a)` (this binds `a` and `b` then uses `a` as the body). An operator with variable valence binds, well, a variable number of... variables. For example, `variable(pattern(a1; a2). a1)` binds two variables, then uses one of them as the body. In a fixed binding position, you introduce exactly one variable for every binding position. But in a variable binding position, you use a pattern instead (patterns, by their nature, can bind any number of variables).

A variable valence operator can only have one binding position, meaning I couldn't have written `variable(a*. b*. a)`, though `variable(a*. a)` or `variable(b*.a )` would be okay. I'm not sure what my justification was for this restriction. I think this is something I was confused about.

It was also the case that you had two choices when it comes to arity: fixed or variable arity.

``````example :=
| fixed(a; b; c) // fixed arity
| variable(a*)   // variable arity
``````

A fixed arity operator always has the same number of children, for example `fixed(a; b; c)`. A variable arity operator has a variable number of children, for example `variable(a1; a2)`.

A variable arity operator can only have one child sort, meaning I'm not allowed to write `variable(a*; b*)`. Why? Because we use `;` to separate subterms, so there's no way to tell when the `a`s end and the `b`s begin.

### The new way

That probably seemed a bit more complicated than necessary. In my change I removed both of the restrictions, so now you can write:

``````example :=
| variable_valence(a*. b*. a) // variable valence with multiple binding positions
| variable_arity(a*; b*)      // variable arity in multiple slots
| both(a*. b*. a*)
``````

A few example terms:

``````variable_valence(a_pattern(a1; a2). b_pattern(). a1)
variable_arity(a1, a2; b1, b2)
both(a_pattern(a1; a2). b_pattern(). a1, a2)
``````

Notice that we've now introduced commas (before the only separators were `.` and `;`). Previously you had to use `;` to separate children in a variable-arity operator, but now we use `;`s to separate "slots" (each of which holds repeated terms of the same sort) and `,`s to separate terms within a slot.

Note that `variable_arity(;)` is now a valid term. This raises the question in my mind of whether we should specify 1-or-more repetition (`+`) in addition to the 0-or-more repetition (`*`) that we currently have. Happily, this is strictly a generalization, so we can add it later.

### Conclusion

Overall I think I'm happy with this new system. My main hesitation is this nagging feeling that people will find this system overly complicated but in a new way. I think you'd be justified in asking what the deal is with `.`, `,`, and `;`.

However, as I'm in the mood for rethinking things, I've begun to think about the purpose of the abstract syntax system. That's what I plan to talk about next time.