Am Mittwoch, den 12.07.2017, 16:15 -0400 schrieb Brandon Allbery:

On Wed, Jul 12, 2017 at 4:11 PM, Wolfgang Jeltsch <wolfgang-it@jeltsch.info> wrote:
I had thought about this possibility already, but then concluded that this was not the case, since types of the form a -o b were not supported. However, when looking at the diffs, I discovered that at the moment, only the Unicode syntax a ⊸ b is understood.

"-o" is going to give the lexer fits. Come up with a purely symbolic version.

It was not me who invented the syntax “-o”. Actually, I do not like it either. While it nicely resembles the lollipop (⊸), implementing it requires stealing syntax. This syntax stealing is worse than the syntax stealing of, say, hierarchical modules. With hierarchical modules in place, you have to use spaces in function composition, but this is reasonable anyhow. However, with “-o” as a lollipop alternative in place, you have to write the negation of o with a space, which is awkward.

Alternatives for “-o” I can think of are “~>”, “-:”, and “-*”, the latter resembling the magic wand operators in the logic of bunched implications and in separation logic, which are similar to the lollipop in linear logic.

All the best,

Wolfgang