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:
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?
- 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.