Unicode type-level infix operators

[toastal]

Namely type-level operators ∀ and → for forall and -> respectively--and maybe subjectively others outside of type-level like ∷ for :: and ∘ for <<.

(==): : forall a . [std.prelude.Eq a] -> a -> a -> std.types.Bool

becomes

(==): : ∀ a . [std.prelude.Eq a] → a → a → std.types.Bool

[Marwes]

Not a fan of using unicode symbols, it just becomes a hassle to write them. Granted, I have never looked into how to make it possible but just the fact that it is something one needs to look up is a pretty big problem.

Having it as an alternative syntax might make some sense but I personally rather stick to one way of doing things. Encountering code written by somebody using unicode when you aren't using it becomes a barrier to entry so I rather avoid that.

It seems more plausible that an editor can translate -> etc to unicode characters on the fly while still keeping ascii symbols in the source code.

[toastal]

Is it possible to create your own type-level infixes? The others can be made with an alternative prelude

I'm actually pretty used to either variety dependent on project (preference for Unicode via ctrl+k in n/vim), but Agda uses it heavily, PureScript supports many out of the box for type-level, and so can Haskell via the Unicode language extension. If both ASCII and Unicode supported, I don't see why there’d be a collision.

[Marwes]

Is it possible to create your own type-level infixes?

No, never really thought about it before since I never felt a need. I don't really object to adding infix types, however for me it has rather low priority. Could be nice to have :: as a constructor for List for pattern matching on it. It could at least be a function for constructing lists now but it seems I forgot to add it to std https://gluon-lang.org/doc/crates_io/std/std/list.html .

For unicode operators specifically they would need to be added to the lexers list of valid operator characters. Since unicode is already allowed in identifiers I suppose it just consistent to allow them in operators as well 🤔 .

: is a keyword operator however (I guess -> is as well, in lambdas \x -> x and match alternatives) so any unicode alternative would need an explicit blessing to work which makes me a bit more skeptical than plain unicode operators but I don't know how rational that is.

[Marwes]

I don't see why there'd be a collision.

It is not about a collision.

If I want to contribute to a library which uses unicode symbols and I am not used to that then that is a barrier to entry. With that drawback I am a bit skeptical to embracing unicode.

[toastal]

For context with PureScript & Dhall, their formatters allow you to specify something along the lines of ascii | unicode | as_authored in configuration options which assists & enforces the formatting in the project which can lower barriers to entry (not that asking for help would ever be off the table). Not code is library code either looking for contribution, but wants to be concise & easy to read. Personally I (still) find it clearer & more accurate to choose the ‘correct’ glyph like → over -> as I don’t really mean dash + greater than, I mean arrow pointing right. This is a product of keyboard layout limitation as with a pencil & paper, most folks would draw a real arrow where both lines attach (hence why a Unicode character exists). Some folks thru layers, compose, digraphs, character maps, formatters, etc. no longer find this to be a barrier.