APL386 Unicode – An APL Font

https://www.pckeyboard.com/page/product/USAPLSET

I would argue that difficulty in reading code and knowing what symbols represent what operations is a much more pertinent consideration. And though neither is especially mnemonic (can you really have a mnemonic for something as abstract as 'sort'?), it's much clearer that single-character grade down (⍒) is the reverse of single-character grade up (⍋), than for digraphs (/: and \:). (It's also easier to parse symbols when they're only one character.) Not least because unqualified / and \ represent very different operations—the first is reduce, and the second is either scan or prefix—as do /. and \.; so there's no precedent for it.

And so, assuming you accept the obvious superiority of graphical/unicode representation of symbols, the digraph method for typing them becomes superfluous. You now have to associate the mental concept of grade with two completely separate representations: the graphical representation of the completed character (⍋) and the ascii representation which you type (/:). You can't escape the latter, because every time you type a grade, you'll see the '/' on screen for a moment before you type the ':' and the character gets digraphed.

I mentioned in the beginning that you can configure your editor (and repl) to automatically replace digraphs with their associated symbols (so /: automatically gets replaced with ⍋). On face, this seems functionally equivalent to the ligature suggestion, but it's not. Mainly, it affords flexibility. If you want to type digraphs in your environment, you can, all my criticisms aside. But I can configure my environment to use an alternate keyboard layout, avoid complicating my editor environment by introducing ligatures, and we can work together seamlessly. Doing it that way also adds flexibility to the language; if ⍋ is the single canonical representation of 'grade up', and / and : are separate symbols with their own unique semantics, then they can be freely juxtaposed. It'd also be somewhat of a pointless indirection, to have ascii digraphs underlying what are essentially unicode-pictorial representations.

(Note: I said only 'digraphs', for clarity, but everything I said applies also to trigraphs, of which j has a couple.)

Not only does it have it, it has it in (what I feel) is a really accessible way. Seen a symbol and you don't know what it is or how to reproduce it? Enter "?" and paste them symbol into the repl and it'll tell you what's it's called, the shortcut to make it, what it does, and the equivalent non-symbol function name.

https://juliamono.netlify.app/

Using Sized Types you can do pretty much anything in Agda though. It's not technically Turing complete since all programs are proved to terminate but you can go very far with it. I really like it because it gives very robust guarantees which makes it very easy think about the state of your program.