Default values for record fields

[lukaszcz]

It should be possible to provide default record field definitions in record type declarations. It should be possible to define default functions using the ordinary function definition syntax. This is especially useful when defining traits. For example, in the Ord trait we would really like to have separate fields for <, <= and == with default definitions, because e.g. for numbers they have more efficient implementations than matching on the result of Ord.cmp.

trait
type Ord A := mkOrd {
  cmp : A -> A -> Ordering
  (<) (x y : A) : Bool := case cmp x y of {
    | LT := true
    | _ := false
  };
  ..
};

[janmasrovira]

We have discussed online some syntax options for record default values.

1. Braces around implicit arguments with default values.
   • Pros:
     1. Consistent syntax where we have {} around every implicit argument. In fact, it is the same syntax that we use in function definitions on the left of the :.
   • Cons:
     1. Can be a bit ugly/confusing with braces around multiline functions.
     2. Probably does not feel natural at first. A good error message can help with this.
2. No braces around implicit arguments with default values.
   • Pros:
     1. Arguably the most intuitive syntax. Intuitive in the sense that it is the syntax that a new user would most likely try before reading the documentation.
     2. Pretty.
   • Cons:
     1. Inconsistent with the syntax of implicit arguments without default value. I.e. If we have defined a field {A : T} for some record and we want to add a default value, we will need to remove the braces, which seems a bit odd.
3. Optional braces. This goes against uniformity and it can be too confusing.
4. It was suggested that we could rethink the syntax of implicit arguments and default values in a more general way with the goal of finding a syntax that feels more natural in all the parts of the juvix syntax. There were no concrete suggestions in this direction yet.

The team was split mostly between 1 and 2. We decided to go with 1 as a temporary implementation and adapt the syntax as needed in the future.