Are there any languages that make fluid use of linguistic context, as in overloading variables/symbols, type-specific sub-languages/operations/functions? I brainstorm here just because variable names tend to get long and complicated in any language, making thought too verbose. For instance, ‘Maybe Int = Just Int | Nothing’ seems incredibly verbose for something that gets passed around a lot in Haskell. So if there is anything that makes variables/function names/types easier within specific contexts —at the cost of readability but making experimentation easy — that would be greatly appreciated

most theorem provers I think fall into this category, e.g. lean https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html#notation

In my digital scientific notation Leibniz (https://github.com/khinsen/leibniz), I have tried to imitate the habits of the mathematical/scientific literature: every text introduces its whole notation explicitly, without any defaults nor any reuse of notation from other texts. If you want to write anything in Leibniz, you have to compose your linguistic context explicitly. There are no hierarchical namespaces either, intentionally, to discourage the building of large reusable libraries that nobody can fully understand anymore.

languages which can overwrite code like Lisp can of course overload symbols, and is well known to be one of the most flexible languages around. Postscript also allows for redefinition of symbols freely. But the king of brevity in terms of languages is perennially FORTH, whose programmers take delight in rewriting the meaning of + temporarily, and the results are incredibly impressive in both speed and compactness. The problem with FORTH is that it is basically a write-only language, and it is super hard to understand your own code a month later, much less other people's code, because you have to keep in your mind what is on the stack, and how many operators are consumed by each operand. Another language which is highly flexible is Red/Rebol. In my efforts to develop my Beads language i have moved in the complete opposite direction so that any feature which makes things harder to read is removed, and the whole thrust is to make programs minimal while promoting clarity. For example + in JS means add OR could mean string concat; i use + for add, and & for concat so you can't mix them by mistake (or cause ruinous implied type conversions which JS does so readily).