Naming *and* notation conventions

[jamesmckinna]

This is a placeholder topic for the time being, prompted by #509 and the appeal to its implied style-guide convention, in #3060 .
UPDATED title while thinking more about

• avoid Unicode in favour of prefix ASCII names #2691
• [ add ] 'lax squares' in Relation.Binary and their horizontal/vertical compositions #3093
• the kinds of things brought up by the post below and its realisaiton as [ refactor ] make Data.List.Base.[_] a pattern synonym #3095

[jamesmckinna]

Eg. 'singleton' container constructors List.[ x ] etc. (I've commented on this in various places before, but I just can't find them now!):

• I would personally prefer to standardise on using the Applicative/Monad interface to name such things as pure (UPDATED: @JacquesCarette has persuaded me to use singleton instead...)
• ... but to permit alternative syntax, for which the obvious prototype would be

  pure-syntax = pure
  syntax pure-syntax x = [ x ]

• the grit in the oyster being, of course List (but also Vec, maybe Tree as well, depending on where we sit in the realm of existing concrete containers-as-data definitions), where, at present, [_] is given as an infix (an 'ex-fix'?) function definition

I personally think that giving up a function name (to clarify: adding something to the namespace and thereby losing/sacrificing a potential name for something else), rather than have it as (optional!) syntax, is a mistake. I especially think so in the cases such as List, where it can, and I think should, be given instead as a pattern synonym, so that it become available as a possible pattern-match... see #3095

The alternative to pattern synonyms would be to write custom views for each kind of container, so that the empty/[_] cases are singled out for special treatment, but in the absence of any well-defined general such treatment, I'd stick with having pattern [_] x = x ∷ [] instead.

See also:

• Feature request: 'computed patterns' agda#7061
• Possible enhancement for [_] in Data.List/Vec/Vector #1497

[JacquesCarette]

Can you explain / justify why you think pure is somehow better? Over say singleton? It was a (huge!) mistake in Haskell to double-down on 'Monad'. Isn't this repeating the same mistake? I'm a big fan of KISS on interface design, and keeping all the fancy stuff on the inside.

[jamesmckinna]

Ugh. No, I can't. Mindless herd behaviour/haskell 'legacy' thinking (which does nonetheless help us make a bridge to one large(r) group of potential users...).

I'd be happy/happier with singleton if ... it consumed less ink (Wadler, after Tufte I think), but I guess that's why I no longer (myself) particular care about the actual name, given that I would always choose the symbolic [_] form... and yet it seems important to provide a memorable-yet-neutral ASCII name. Do please modify the proposal to advocate instead for alternatives, esp. on #3095 ! UPDATED: I see that you did!

There's a separate discipline for library developers about whether we stick with the 'internal' name, or make free use of the (symbolic) alternatives, and that also seems part of (the consequences of) #2691 . I wish I felt I had a settled clear (and autocratic!) position that I could advocate for, but part of your (expanding!) Discussions balloon is that it's a space currently for speculation more than decision.

But part of your appeal to KISS also seems to have a/the 'converse' alternative (Unix again, but then also Don Norman's "why I hate Unix"): choose short names internally, and for 'client-facing' (the endless Data.X vs Data.X.Base tension/debate) modules, use qualified import/renaming directives to turn 'internal's into 'external's... pure can always be called singleton instead, in deployment contexts where that's a 'better' name for the mode-of-use... and we're back to the tension between having a common vocabulary for the Container perspective and the Effectful one.

(Sidebar: my other legacy, from 40+ years ago, would be always to call pure instead η, but that's unfortunately very unlikely to gain traction on most users... but I am willing to argue strongly for ι for 'injection'/monomorphism, and correspondingly π for 'projection'/epimorphism in our ongoing addition of sub- and quotient- gadgets to Algebra.*...)

For free monads, I've historically argued, with some success with some people/audiences, for var and con (for 'variables' and 'constructors') as 'canonical'/preferred names, and maybe var is indeed preferable to pure... except for all the other (meta-)mathematical contexts in which 'being a variable' has a distinct flavour (but not really, semantically!)...

In turn, can you say why you think haskell made a (huge?) mistake in structuring things on/around Monad? (Ob which, for better or worse, pure is better than return, ... I think?)

[jamesmckinna]

'ASCII vs.Unicode' or: 'prefix vs. mixfix' or 'prefix and mixfix'...

Up until now, I've been an enthusiastic advocate for Agda's support for mixfix / symbolic renderings/representations of concepts, and I still think that the library rightly makes good use of such facilities... but part of my encouragement to @jwaldmann for #2691 stems from having some conscience about whether our use of symbols is always... helpful.

So I've started to think (with the 'singleton' above as a specimen, and simple, instance of the phenomenon) that we should consider supporting both textual and symbolic names for concepts/definitions.

There are principles and pragmatics (esp. wrt UX, but also specifically what additional support/plumbing/infrastructure, eg. dictionaries/glossaries, might be necessary to support such redundant recoding) to consider, so this is a prompt to think/discuss further...

[JacquesCarette]

It is very easy to abuse 'symbol soup'. I would not want to give up the ability to use unicode+mixfix. But I'm all for being cautious. Having some textual alternatives is not a bad idea.

But do also take a look at agda-unimath. Just as we sometimes err on the 'symbol soup' side, they create other horrors.

[jamesmckinna]

Well, I think my take on 'unicode+mixfix' is indeed that we want a 'both/and', but that for many/most symbolic declarations, a textual/ASCII alternative is ... desirable, not least for deployment contexts (eg for beginners) where 'simplicity' perhaps attracts a higher premium than 'information-density' (with nods to @gallais for advocacy on behalf of the latter).

As the discussion on #595 and related issues seems to have revealed, even the tension between 'flat' definitions (the legacy of 150+ years of first-order logic, moreover a tradition in which definitions/'abbrevation's/information-compression are taken as 'mere' pragmatics, or otherwise finessed away), and the customs/habits of 'typed; higher-order; definitional' style which the FP/HOL/type-theoretic style have made commonplace in the last 50, are real, and perhaps under-appreciated.

Yes, I know you have advocated for selective/progressive unfolding/normalisation as a device to mediate between the two, and at some level, that's 'obvious': in a theory that is so thoroughly underpinned by making definitional equality work harder, it's easy to come to rely on the kind of internal expert reflex/muscle memory that 'sees through' definitions, even when beginners/outsiders might find such habits don't come easily... much as some people (myself included!) don't always respond, without effort, to the compression/decompression flex that is/seems to be demanded by diagrammatic reasoning in category theory.

(Sidebar on 'free rides': just as 'every abstraction carries a cost', so too every notation. In theory/philosophy of mind, the power of diagrams comes from 'making tacit conclusions from hypotheses encoded in the image directly/immediately accessible from the form of the image itself', that is, 'deduction for free'. Exponents of various notations often seem to neglect to pay attention to how much such 'free rides' actually cost, and ... perhaps more, but for another time)