On Wed, Jul 12, 2017 at 4:11 PM, Wolfgang 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
Am Mittwoch, den 12.07.2017, 16:15 -0400 schrieb Brandon Allbery: 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