Naming conventions for state-like record constructors

[carlostome]

trafficstars

There seems to be no convention on the naming of record constructors for state-like record types. This make it hard to mentally navigate some of the rules.

We currently have:

⟦_,_,_,_,_⟧ᵉ' for EpochState
⟦_,_,_,_⟧ᵘ for UTxOState
⟦_,_,_⟧ᵈ for DState 
⟦_,_,_⟧ˡ for LState 

(There are probably more)

[WhatisRT]

I agree it's a bit messy, but I'm not sure how to do better here...

[HeinrichApfelmus]

I would group this issue under #763 .

The question is: How do we decompose a record into its constituents in a human-readable and -memorable way?

My personal preference is to use whatever default record the language (Agda) provides, i.e. plain record, because that default has a life outside of our specific domain. Unfortunately, the default tends to be rather verbose. That's why most rules in our domain use the "funny brackets" syntax, e.g. ⟦_,_,_,_,_⟧, sometimes with post-formatting for vertical alignment even.

There are a few rules that use record, though mostly for updates:

[WhatisRT]

Generally I like record updates as well. Their downside is that they offer less presentation options than the vectors which, paradoxically, can lead to them being harder to understand. Here's an example:

Compare this with applyRUpd (btw. apparently this is broken again on master, @carlostome or @williamdemeo can one of you have a look?):

Both of these are nested record updates, and the one at the bottom is the more complicated one but I find it much easier to understand what's going on. I find that first giving the shape of something and then describing what to change in that shape is a fantastic way to present record updates, in particular nested ones. Sadly, I don't really know how to have a similar presentation if you don't have some kind of pattern-match, or of the match is far away from the update.