Standardise record constructor names

[mechvel]

For record IsGCD in Algebra.Divisibility, the constructor is gcdᶜ .
But for some other records, the constructor is of kind mk<Foo>.
Probably we need to make it uniform.
Personally, I vote for ᶜ .
Because a) it abbreviates "constructor", b) it is shorter.
?

[zraffer]

A little crazy solution.

Currently field projections (destructors of coinductive types) are distingushed by postfix notation prefixed by dot like this: arg .fst , arg .snd

It would be lexically perfect if we were able to use a fully mirrored notation for constructors of inductive types like this: Left. arg , Right. arg - i.e. as prefix operator postfixed by dot.

As far as I'm aware none languages use this notation. I understand this should be a (questionable) request for agda repository, but here is the place where the discussion of constructors was started.

[gallais]

Because a) it abbreviates "constructor"

I don't think the proposal is fully fledged. Is it:

• Take a record type name that starts with Is
• Drop the Is prefix
• Make it lowercase
• Append the character ᶜ

?

b) it is shorter.

It's shorter by 1 character but it's more annoying to type.

[mechvel]

Not precisely. I mean

1. Change the first letter in the record name to the lower case.
2. Append the character ᶜ
   Example:

record IsGCD ... where
    constructor isGCDᶜ

Generally, <foo>ᶜ
where <foo> is a name starting with a lower case symbol and having much in common with the record name.

b) it is shorter.

It's shorter by 1 character but it's more annoying to type.

But mkFoo looks like an ordinary function name, as not necessarily a record constructor.

[MatthewDaggitt]

@mechvel thanks for raising this. I agree, we should be consistent about how we name the record constructors.

I'm with @gallais and that we should go with mk as a prefix to the record name. It's two easy characters to type "mk" rather than three, two of which are hard ones "^c".

I don't quite know what you mean by "it looks like an ordinary function name, as not necessarily a record constructor.". In Agda the set of valid names for record constructors and functions are identical?

[mechvel]

It is desirable to have a final decision announced.

[mechvel]

I don't quite know what you mean by "it looks like an ordinary function name, as not necessarily a record
constructor.".

Seeing (fooᶜ x y ...) the reader would understand concretely that this is a record construction from the record fields.
Seeing (mkFoo x y ...) the reader would imagine generally some function that makes something from something , for example, makes an instance of StrictTotalOrder from DecTotalOrder, Foo from Foo' ...
The are many kinds of entities that can be made from other kinds of entities.
This is a meaning tradition of the word mk.
For mkFoo, the reader can think of Foo as of a record or of a relation or of other things.
And fooᶜ has not such an indefinite tradition, it will be understood that Foo is a record.
(?)

[MatthewDaggitt]

In response to your comments in #1392 let's go with mk. I'l l add an entry to the style guide at some point.