since this thing is intended for doing bidirectional syntax transformations,
that leads to an interesting question, should it be able to translate between A -> B -> C
and reverse arrow notation B <- C <- A
Type arrows may be reversed, thus writing c <- b <- a is equivalent to writing a -> b -> c.
The argument for it is that tis would be nice, because then composition:
o: (b -> c) /\ (a -> b) -> a -> c can be read in right-to-left fashion: o: c <- a <- (c <- b) /\ (b <- a)
An arguments against include that its weird, and that it isn't a simple like the ASCII <-> unicode translations,
in that it implies flipping the input and output type
since this thing is intended for doing bidirectional syntax transformations,
that leads to an interesting question, should it be able to translate between
A -> B -> Cand reverse arrow notation
B <- C <- ATwelf meta-logical framework
The argument for it is that tis would be nice, because then composition:
o: (b -> c) /\ (a -> b) -> a -> ccan be read in right-to-left fashion:o: c <- a <- (c <- b) /\ (b <- a)An arguments against include that its weird, and that it isn't a simple like the ASCII <-> unicode translations,
in that it implies flipping the input and output type