avoid Unicode in favour of prefix ASCII names

[jwaldmann]

(... you asked for this in #2690 (comment))

I do use Agda, and I do teach it (not a full course though). While teaching, I do avoid stdlib, mainly because I rather show to students how to build a (very small) subset of concepts from scratch. And, to a much smaller extent - because of the reasons I mentioned: unicode symbols are hard to read (to discern optically), to pronounce, to write (on a keyboard). To some extent, I can avoid typing unicode symbols if mimer suggests them. In all other cases, I need to remember how to type them (this wastes brain space), or I have to copy-paste them (this wastes time).

[gallais]

In all other cases, I need to remember how to type them (this wastes brain space), or I have to copy-paste them (this wastes time).

Emacs has a M-x describe-char command (bound to C-u C-x =) which will give you info on
the character under your cursor, including how to input it.

I think we should avoid « hard to discern optically » conflicting characters but IMO, and precisely
for readability, it's important to have information-dense symbols rather than names that are
long-strings-of-charaters.

[jwaldmann]

character under your cursor,

yes - if I have it under the cursor. What if I'm reading the character elsewhere? E.g., other file - need to navigate there. Or, worse, totally different medium, e.g., student reads it from a demonstration in class, or, looks at lecture notes in some other format (printed book,ebook on tablet that has no emacs).

The concept of a name is that it is a reference to another entity (the theorem). This is less useful when I can write the name only by actually navigating to the entity first (the module that contains the theorem) to copy its letters from there.

Naming things is hard. At one end of the spectrum, there's Java's DoubleStream.DoubleMapMultiConsumer, at the other end - APL, but - that was designed for special keyboards, so you had the symbols right in front of you, always. ( https://aplwiki.com/wiki/Typing_glyphs , "... did not hinder students in any measurable way" ).

[gallais]

I agree that if you are publishing static material you may want to throw in additional
information on how to type some of the symbols. It's not unheard of to have e.g.
mathematical texts explain how a convenient notation is pronounced.

Then again I would presume that your textbooks & so on come with libraries and
that you're not expecting your poor user to retype all of the boilerplate code just
to be able to tackle the exercises. And these libraries should then be loadable in
your editor of choice via appropriately ASCII only import statements.

I maintain that, to me at least, information dense symbols corresponding to already
established mathematical intuitions are much more readable than basically pure LISP.
But we're rapidly approaching almost chemically pure bikeshedding.

[jamesmckinna]

But we're rapidly approaching almost chemically pure bikeshedding.

Well, yes maybe, but...

... I take seriously the didactic/pedagogic aspects of our choice(s) of names and 'house-style', wrt raw syntax, intended semantics, and these other very thorny questions of ux pragmatics (I personally hate having to use M-. as a navigability/surveyability affordance, precisely because of the loss of context.

And accommodating different user styles ought to be a long term goal, esp if eg we could be more principled, as well as more flexible, in accommodating 'pure Lisp' side-by-side with suitable syntax declarations... but I suspect give the current state-of-the-art, that's still too unwieldy/unworkable in practice?

[jwaldmann]

One might wonder: in fully qualified names, we have the "Java Enterprise" naming style right until the very last dot, and APL style only after that, viz. Data.Empty.Polymorphic.⊥ If short ("information-dense") names are good, then why does this not apply to modules?

[jamesmckinna]

One might wonder: in fully qualified names, we have the "Java Enterprise" naming style right until the very last dot, and APL style only after that, viz. Data.Empty.Polymorphic.⊥ If short ("information-dense") names are good, then why does this not apply to modules?

AFAIU, essentially because existing OS conventions regarding hierarchical folder/directory structure favour using ASCII names, not 'symbolic'/'information-dense' ones... so there's a tension between conventions internally to Agda and Agda<->ambient OS ...?