The Syntax Bikeshedding Dojo, round 2: Metavalues/Enriched values (modules)

[tweag]

The Syntax Bikeshedding Dojo, round 2: Metavalues/Enriched values (modules)

[thufschmitt]

I quite like the proposed syntax. A few questions/remarks (/!\ bikeshedding ahead):

1. Do we want to be able to abstract over parts of the schema. Say I have 12 options that have the same type and the same default value, should I be able to factor these? I assume the current syntax allows this (or at least could be easily extended to allow it), but the proposed one quite likely doesn't, or not in a natural way.
2. Is having zero metadata allowed? Because if so the proposed syntax has a natural way of expressing that (just don't put anything between the option name and the semicolon), while the current one less (Well I assume you could pass in an empty tuple, but that's a bit akward)
3. It feels a bit weird to have a really different syntax between { foo = 1;} and { foo | default 1; }, while they are nearly the same thing. Esp. if there's a whole scale of priorities like in Nix. Maybe it would make sense to have something like { foo = 1 | priority default; } or something like that

[yannham]

Do we want to be able to abstract over parts of the schema. Say I have 12 options that have the same type and the same default value, should I be able to factor these? I assume the current syntax allows this (or at least could be easily extended to allow it), but the proposed one quite likely doesn't, or not in a natural way.

You are right, the current version is able to do that, as opposed to the new proposal (at least as it is currently). I don't know how frequent this can be.

Is having zero metadata allowed? Because if so the proposed syntax has a natural way of expressing that (just don't put anything between the option name and the semicolon), while the current one less (Well I assume you could pass in an empty tuple, but that's a bit akward)

It is not currently allowed by the AST: a field can contain a usual value, or a meta-data (docstring, contract, default value), or some combinations of the two, but can't be nothing. I guess a field without attribute nor value would just require a presence ? This can be encoded currently using a Contract(Dyn), since a contract does require the presence of a field, and any value satisfies the Dyn one. We could make a field without attribute to be syntactic sugar for this.

It feels a bit weird to have a really different syntax between { foo = 1;} and { foo | default 1; }, while they are nearly the same thing. Esp. if there's a whole scale of priorities like in Nix. Maybe it would make sense to have something like { foo = 1 | priority default; } or something like that

I don't really like putting the priority in suffix position. Maybe just put the priority at the same level as the others ?

{ 
    foo | doc "blah"
        | type #foo 
        | priority default
        = 1;
}

[thufschmitt]

I don't really like putting the priority in suffix position. Maybe just put the priority at the same level as the others ?

{
foo | doc "blah"
| type #foo
| priority default
= 1;
}

Ah, I assumed that the general syntax was to have the meta after the values. But it makes more sense that way, indeed

[hanshoglund]

Some prior art:

• https://clojure.org/reference/metadata
• https://python-sprints.github.io/pandas/guide/pandas_docstring.html

[aspiwack]

I think that there is an attribute missing: value, such that foo = blah means foo | value blah.

I'm not sure whether we want to mix | and = in the same list. But it may be worth it. (my first instinct is to have either | attr or =).

I do think that | default blah makes sense as it is typically how you present documentation, why not write it this way? Even if it doesn't make much sense to have both a | value and a | default.

However, I can see a point in the syntax proposed by @regnat . That is, instead of having (at most one of) | value and | default. Have | value and | priority, and priority could take a natural number (or infinity).

• If priority is not specified, then the priority is infinity
• When merging two fields with values, if they have the same priority, then merge recursively
• When merging two fields with different priorities, take the largest priority (default is 0).

This lets us emulate arbitrary overloading of values. (though if a value is to be overriden, you still need to prepare for it, so it's not perfect yet).

[thufschmitt]

If priority is not specified, then the priority is infinity

We could also have an arbitrary default priority (or make priority a relative number with a default of 0) so that we can override values defined with =. IIrc that's what NixOS modules do.

[yannham]

We had a bikeshedding coffee-break yesterday with @regnat and @garbas. Some ideas that popped up:

• # is nice to syntactically distinguish contracts. We would require it at declaration time, as in let #mycontract = fun l t => ... It could also enforce that it has type Label -> Dyn -> Dyn (which is not very restrictive) at typechecking phase (but probably without adding runtime casts, because adding runtime checks inside runtime checks doesn't sound nice).
• in the same vein, impose a case for contracts/types/values. Maybe contracts and types should be both capitalized while values wouldn't be allowed to start with an uppercase letter.
• don't use any keyword for type/contract: value | Num -> Num or value | #Url. Or use a type for contract specified as types, as value | type Num -> Num and nothing for contracts as before, if it is clear in the language that # = contract.
• it could make sense to have a different syntax for Asssume-used-as-runtime-check and Assume-used-as-type-coercion, since these are quite different usages.

[yannham]

As a last minute thought before implementation, the pipe may clash with the following potential future features:

• Union types/contracts: not in the general case, since the result of @teofr 's exploration is that this is not a good idea, but we can imagine having such an operator defined for specific cases at some point, such as the union of flat contracts, which is trivial to construct: #Num | #Str. In this case (x | #Num | #Str) becomes ambiguous.
• Tagged unions: it is customary to define the diffferent constructors of an algebraic datatype using |, although some languages do it differently, such as Rust.
• Pattern matching: it is also customary to group patterns that receive the same treatment using |.

The first case can be disambiguated and the last two points would not result in an actual grammar ambiguity since the pipe is used in distinct syntactic constructs. But I imagine overloading this operator too much could make the syntax confusing.

[yannham]

Close by #266.