Proposal for cleaning up Term::Id versus Term::App and the concrete syntax of function calls with zero arguments

[wilcoxjay]

The current situation

Declaring functions with zero arguments versus declaring constants

Consider following two similar global declarations

mutable f(): bool
# or
mutable f: bool

Currently these two different concrete syntaxes for a function declaration parse to the same declaration AST, namely RelationDecl {mutable: true, name: "f", args: vec![], sort: Sort::Bool}.

Defining a macro with zero arguments

Currently, definitions must use parentheses, even if there are zero arguments.

# this is allowed
def f() -> bool {
    true 
}

# this is a syntax error -- expected '(' after 'f'
def f -> bool {
    true
}

Calling a function of zero arguments versus referring to a constant

There is a similar situation at the term level. Consider these two terms:

f()
# or
f

But this time, the current implementation handles it differently. The first term parses to the AST Term::App("f", vec![]) while the second term parses to the AST Term::Id("f"), which are not equal and indeed are never converted between each other.

The current sort checker forbids the App AST with zero arguments, so while the first term above parses, it does not sort check.

Proposals

Overall, the examples above show that the current situation is messy, both for end users (who may be confused by the multiple syntaxes, some of which are only allowed in some places and not others) and for flyvy developers (who have to deal with multiple AST nodes that should intuitively be equivalent but are not).

I have had a few discussions with all of you about this, and there are a few ideas for how to improve things.

Eliminate redundancy in the AST for terms

I think everyone I've talked to agrees that we should choose just one of Term::App(f, vec![]) and Term::Id to support. Different people prefer different versions of this.

• Idea A1: Eliminate Term::Id entirely. Parse all constants and variables to Term::App(x, vec![]).
  • Downside: it may feel strange to flyvy developers who are used to a more traditional AST representation of variables that a logical variable is represented as a function call of zero arguments internally.
  • Downside: variables really are different from function calls. For example, you can substitute for a variable but not for a function call. Variables go in and out of scope, but functions cannot be introduced in any local scopes. So some code would need to branch on the length of arguments anyway.
• Idea A2: Make it an invariant of Term::App that the argument list is non-empty. Parse function calls of zero arguments to Term::Id(f).
  • Downside: if we allow the end user to write f() then it might be surprising to flyvy developers that this does not parse to a function call.
  • Downside: sometimes we want to handle variables just like function calls of zero arguments. Having separate AST nodes makes the code have to repeat itself. For example, if you want to traverse the AST and check whether there are any temporal operators used, then you will treat variables exactly like a zero-argument function call, but this design will force you to distinguish the two cases anyways.
• Idea A3: Keep both. Use Term::Id only for bound variables (quantified variables and definition arguments) and use Term::App(f, vec![]) for global constants (ie functions of zero arguments) (and macros of zero arguments?).
  • Downside: This distinction feels weird.
  • Downside: This distinction cannot be easily implemented by the parser, which lacks any scope information. So we would have to parse to some intermediate representation and then resolve names to get into an AST like this.

Overall I prefer Idea A1. I'm also ok with A2, but I am slightly opposed to A3. What do other people think?

Eliminate redundancy in the concrete syntax of terms

Should we allow the user to write both f() and f and parse them to the same thing?

• Idea B1: Allow both and parse them to the same thing
• Idea B2: Allow only f
• Idea B3: Allow only f()
  • Downside: end users may feel that it's strange that "there are no global variables, only global functions"

My preference is B1. I like B2 almost as much. I don't like B3 as much, but I'm not opposed to it.

Consider eliminating concrete syntax redundancy in function declarations

Should we allow the user to declare a function of zero arguments with parentheses or not or both?

mutable f(): bool
mutable f: bool

• Idea C1: Allow both and parse them to the same thing (this is what we do today)
• Idea C2: Allow only f
• Idea C3: Allow only f()

My preference is to match our choice at the term level. So if we choose B1, we should also choose C1, etc.

Bring macro definition syntax into agreement with function syntax

Should we allow declaring macros of zero arguments without parentheses?

def f() -> bool {
    true 
}
def f -> bool {
    true
}

• Idea D1: Allow both and parse them to the same thing
• Idea D2: Allow only f
• Idea D3: Allow only f() (this is what we do today)

My preference is again to mirror the previous answer: if we choose C1, then we should choose D1, etc.

Uniformize the return type annotation of definitions

While we're at it, how about replacing -> with : in the definition return type annotation?

def f(): bool {
    true 
}

• Idea E1: Use -> for return type annotations (this is what we do today)
• Idea E2: Use : for return type annotations

I prefer E2 because we use : everywhere else.

[Alex-Fischman]

I am in favor of A3. The most natural way that I've found for writing Term traversals when I care about this distinction is to first normalize into a form of A3, and then do the traversal (see nullary_id_to_app in bounded). This works well because it then lets me call Next::normalize on the resulting term (moving finite numbers of Primes into the field in App), and this makes it so that I can ignore all temporal operators in my traversals. In fact, I would prefer to also do this normalization on all programs returned from the parser, since Prime (and Next?) can only significantly act on mutable relation applications anyway.

A justification for A3 is that bound variables and relations really are different in many cases (see the A1 downsides), and it should be the parser's job to deal with syntax so that I can worry about semantics. I propose that if we go with A3, we should strongly consider renaming Id to Binder, and also potentially consider renaming App to Global or something similar.

I don't feel as strongly on the rest of the choices, but weakly prefer B3, C3, D3. I do also like E2 more than E1.