agda-stdlib
agda-stdlib copied to clipboard
agda
Standardise record constructor names
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.
?
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.
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
Isprefix - Make it lowercase
- Append the character
ᶜ
?
b) it is shorter.
It's shorter by 1 character but it's more annoying to type.
Not precisely. I mean
- Change the first letter in the record name to the lower case.
- 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.
@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?
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.
(?)
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.
Bumping this to v2.0 as it will be breaking change.
Can't we use pattern synonyms to make it backwards compatible?
Err, honestly I'm not sure. If you think there are no edge cases in which record constructors can be used and pattern synonyms cannot, then I'll believe you. However, we know there are such edge cases when using pattern synonyms to try and deprecate data constructors right?