feedback on SYNTAX.md

[skybrian]

Hi, I'm new to this project and thought I would write about the parts of SYNTAX.md that I found unclear, since it seems to be the closest thing to a language definition.

This is without doing anything else to find the answers; I could probably figure it out, but figured a new user perspective might help. I don't have all the background to understand what's going on, but maybe that's good?

(You don't need to answer my questions if you're going to improve SYNTAX.md instead.)

---

Top-Level definition

my_name: String
   "Victor"

It might be nicer to make this the second example, since it's the degenerate case when there are no arguments.

The name of the top level definition also specifies the file where the definition is. For example Physics.Verlet.step must be either in base/Physics.kind or base/Physics/Verlet.kind or base/Physics/Verlet/step.kind.

Are these files searched in any particular order? What if the same name is defined in two places?

they can't appear anywhere in the program and, instead, must appear at the "global scope" of a file.

Okay, but what if you do the opposite? Can expressions appear at top-level? (In particular, Let and Def.)

Lambda

There are no true multi-argument lambdas [...]

Is this also true of top-level definitions?

You can also omit the name and write just () body

Is this a shortcut for a one-argument lambda that ignores its argument? Maybe say that explicitly?

Application

A function application can also be written using <> instead of ()

Maybe add an example?

An application to a hole

Holes haven't been defined yet. (Add forward reference.)

Also, maybe say something about evaluation order. Is this lazy or strict?

Def

def x = f(42)

It seems like more could be said about macro expansion. What if f is a def? Can 'def' appear in a function? Suppose f is a function argument? Do I need to worry about hygienic macros?

Forall

Forall, or Pi, or self-dependent function, is the type of a function.

This is a little too brief to be understandable. I think what's being said is that these aren't full examples, they are just examples of different ways to write the first part of a function definition, the part declaring the name and type. But that wasn't clear on first reading, and saying that it's "the type of a function" meant that I was wondering if, for example, you might use this syntax to declare an input parameter of a higher-order function.

Also, at this point, I don't know whether "Bool" or "Nat" are considered part of the standard library.

Nat.add is a function which takes two Nats and returns its sum.

Does Nat already exist? Are we defining Nat.add? It says this is a function, but it looks like we might be defining the type of a function? It doesn't seem to specify an implementation, so how do we know that Nat.add returns the sum of its arguments?

Bool.double_negation is a proof that for all Bool, its double negation is equal to itself.

Are we assuming that Bool.not was previously defined?

Also, needs to call out the forward reference to Equal type.

Also, it would be good to refer the reader to the full example that comes later, under pattern matching.

(n: Nat) Vector(Bool, n)

Okay, now we're talking about function types, I think. Shouldn't this be a separate heading?

Is the type of a function that receives a n: Nat and returns a Vector of n Bools.

Maybe call this out as an example of dependent types. (That is, n seems to be playing the role of both an input parameter and what would be a type variable in other languages that use generic types.)

Which is a function that receives a Nat and returns a Nat.

"Type of a function" presumably?

Datatype

Not knowing Agda, I'm not sure what "indices" means here or what sort of datatype Vector is. Maybe this would be better explained in a separate introduction? An example of how a Vector could be used might help.

Case (pattern matching)

Notice that the true case and the false case return different types.

Probably because I'm not familiar with dependent types, I'm not really following what it means to return a different type on each branch. Is the result of this case statement a proof? Does returning a different type on each branch work outside proofs?

Here, Kind evaluated if x then String else Nat with each possible value of x (in this case, true or false) to determine the return type of each branch.

Maybe explicitly say that we're talking about type checking, and specifically that type inference goes from the return type to inside the case statement.

double_negation(b: Bool): Bool.not(Bool.not(b)) == b
  case b {
    true: ?a
    false: ?b
  }

It seems like ?a and ?b haven't been defined yet. (Add a forward reference to Goal.)

Also, the syntax of the return type, Bool.not(Bool.not(b)) == b, wasn't previously defined, so there should be a forward reference to the Equal type.

Formality demands you to provide a proof of not(not(b))==b on both cases. This isn't possible.

Oops, rename Formality -> Kind. Also, maybe say why it's not possible, and why Kind asks for it anyway?

double_negation(b: Bool): Bool.not(Bool.not(b)) == b
  case b {
    true: refl
    false: refl
  }!

Need to add a forward reference to Equal type for refl.

The code above works by creating an extra lambda, it is equivalent to

I don't understand why the lambda expansion of with notation works. Does a lambda somehow automatically do the same specialization as with?

Logging

Note that the order that Debug.logs happen can change depending on the evaluation strategy used by the target language

Maybe add an example and how different target languages would handle it.

If, then, else

I'm wondering about evaluation order here, since the expansion seems to imply lazy evaluation.

Do notation

This seems like a good place to explain some of the built-in monads. It seems like the conversion might be indented to show that it's a bunch of nested callbacks.

New sigma

Sigmas aren't really explained until the next section; forward reference?

Without

This might be explained as sort of like an "early return" in other languages.

Equal.apply

Maybe add an example?

While loops

You can also use get instead of let to store a pair on the state

I don't see get in the example.

[skybrian]

(Not really a bug, but I'm not sure how to tag this.)

[rigille]

Your feedback is very helpful, I'm thinking about the questions you raised. Your issue is better suited to our discussion forum, so I'll move it there