Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

reverse arrow notation? #20

Open
ratmice opened this issue Jul 7, 2020 · 0 comments
Open

reverse arrow notation? #20

ratmice opened this issue Jul 7, 2020 · 0 comments

Comments

@ratmice
Copy link
Owner

ratmice commented Jul 7, 2020

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

Twelf meta-logical framework

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant