Skip to content

reverse arrow notation? #20

@ratmice

Description

@ratmice

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions