Add record declaration syntax support

[jonaprieto]

Example:

type A (B : Type) :=
  constructor1 {
    cfield1 : X1;
    cfield2 : X2;
  }
 | constructor2 {
    cfield3 : Y1;
 };

[lukaszcz]

After implementing

• Optional and named arguments #1991

we might not need or want a separate syntax for record declarations. With the proposed syntax for named arguments a record can be defined as:

type R :=
  Rctr : (cfield1 : X1) -> (cfield2 : X2) -> R;

If there is only one constructor, accessor functions can be automatically generated, maybe with an additional specifier like

record 
type R := 
  Rctr : (cfield1 : X1) -> (cfield2 : X2) -> R;

[lukaszcz]

But perhaps the named argument syntax becomes inconvenient with a large number of fields. So we may actually want the proposed syntactic sugar:

record
type R := Rctr { 
  cfield1 : X1;
  cfield2 : X2;
};

[lukaszcz]

I actually think this is much more readable:

trait
type Encoding (A : Type) := MkEncoding {
  encode : A -> Field; 
  decode : Field -> A;
};

than this:

trait
type Encoding (A : Type) :=
  MkEncoding : 
     (encode : A -> Field) -> 
     (decode : Field -> A) ->
     Encoding A;

[janmasrovira]

I agree with your points.

A couple of extra comments:

1. The record keyword is not neccesary for parsing, we could simply disambiguate based on what's written. The problem then becomes that we don't know if we should generate field accessors or not. But I would say that it is ok to always generate them if there is a single constructor. If we did this, we don't need to record keyword at all.
2. I think it'd be more consistent to use parentheses instead of braces after the constructor name. That way, we would respect the existing juvix convention to use braces for implicit arguments.

[lukaszcz]

2. I think it'd be more consistent to use parentheses instead of braces after the constructor name. That way, we would respect the existing juvix convention to use braces for implicit arguments.

We use braces often for blocks of declarations, e.g., in lets. The fields of a constructor are a bit like such a block of signature declarations. Maybe we could use with here to indicate that we're starting a block of signatures (and to keep consistent with the syntax for updating/creating records)?

trait
type Encoding (A : Type) := MkEncoding with {
  encode : A -> Field; 
  decode : Field -> A;
};

[janmasrovira]

we are not using braces in lets. What blocks of declarations are you referring to?

[janmasrovira]

I wouldn't strongly oppose to braces however. I think they have a big pro, which is that they are often used for record-like structures in other languages

[lukaszcz]

No? Damn, I'm not keeping up with the syntax.

[lukaszcz]

I think I got confused with Core syntax.

But we're using braces in the lambdas, and that's a bit like introducing a block of clause definitions (but the analogy is weaker here).

[lukaszcz]

Braces seem nicer because multi-line parentheses look kind of weird. The parenthesisation is also easier to track visually if you follow the convention:

• paretheses for small blocks (like application in expressions)
• braces for (potentially) big blocks (like lambdas or record declaration/update)

[janmasrovira]

agreed