Skip to content

🌎 Generalized "positions"? #169

Open
@mikeshulman

Description

Since you're rethinking some things about ranges now, I figured I may as well throw this out there.

It occurred to me recently that there may be situations in which the "position" of an error is not a range, or even a single position, in a string or file, but could be something more complicated. In particular, suppose a proof assistant has some kind of graphical or higher-dimensional syntax; in that case the natural "position" of an error would be a pointer or reference to some graphical object. Of course in that case it would be impossible for a generic library like Asai to display such a "position" along with the error -- whatever code is dealing with the graphics would have to do that, as well as deciding how to associate the error to its position, presumably with a custom diagnostic handler -- but it would be nice if the core code that reports errors could be agnostic as to what kind of "positions" are being used, e.g. if a proof assistant is mostly textual but also includes a graphical language for certain kinds of proofs, using the same typechecker for both of them under the hood.

I admit this seems like it might be really hard to implement. Moreover, I expect one could use the current interface for this purpose in a slightly kludgy way, by transforming the graphical input into an internal string that the user never sees and using ordinary positions in that string. The string could be a structured representation like JSON or SEXP that actually represents the picture, or just a string of meaningless characters with a lookup table associating each position to a graphical object. And maybe that's the best way to go. But as I said, I thought I'd throw it out there so it's on your radar while you're rethinking the representation of ranges, in case some brilliant idea occurs to you. (-:

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions