🌎 Generalized "positions"?

[mikeshulman]

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. (-:

[favonia]

Does this amount to making the location type polymorphic? Maybe this can be done with the following change:

Asai.Reporter.Make(Asai.Range)(Message)

where Make is taking two modules. One for locations, and the other for messages.

[mikeshulman]

How would Asai.Tty.Make work then?

[favonia]

@mikeshulman The TTY backend has to work with the current Range module (or something that provides a linear order I suppose?).

[mikeshulman]

I suppose that's all it could do. But I'd want the same code to be able to deal with both textual and graphical terms, so my Range module would include both as possibilities, which means I'd have to wrap the default TTY backend in something else that extracts textual locations when present. I'm not sure that'd be better than just using an internal string representation of picture locations.

[favonia]

@mikeshulman Do you want the TTY backend to display only "textual" ranges and treat all other types of locations as "not having a location", or that it should allow an abstract location to decide its own string representation? For the former case, we probably do not need to change much beyond making the location type abstract. For the later case, we need to change the TTY backend, but perhaps not too much, either.

[mikeshulman]

I like the idea of it displaying only textual ranges and treating other types of locations as "no location", but I'm not sure how that would work in practice without a typecase. If the location type is abstract, how does the TTY backend tell whether a location "is textual"?

[favonia]

The first solution is exactly what you suggested: wrapping the TTY backend. The new type of diagnostics can be ('code, 'loctext) Diagnostic.t. Then, the map function has a new type:

Diagnostic.map
  : ('code1 -> 'code2)
  -> ('loctext1 -> 'loctext2)
  -> ('code1, 'loctext1) Diagnostic.t
  -> ('code2, 'loctext2) Diagnostic.t`

The other solution is that the user of the TTY backend needs to implement to_loctext : loctext -> Asai.Loctext.t or something like that.

---

One problem of treating other location types as "no location" is that a message intended to be displayed at a specific place might not make sense without a location. Maybe it's a good idea for the user to provide a way to print generalized locations instead of giving them up completely.

[mikeshulman]

I guess I could see either of those working. If you feel like trying to implement something here (which I don't think you need to), maybe pick whatever seems best/easiest to you, and I'll let you know what I think?

[mikeshulman]

It might also be useful for locations to mix textual and non-textual information. For example, a component of a graphical proof might include a text box where the user can type a string to be parsed textually, with the resulting term then being used in the meaning of the graphical component. (This is natural, since it can be extraordinarily tedious to use a graphical language for 100% of a proof, so you'd want to be able to drop into text when needed.) Then diagnostics emitted by that text should be associated to the graphical component, but also refer to specific locations in the text.

This is probably easy: the locations contain both kinds of information, and the custom handler extracts the non-textual information before passing the textual information off to Tty. But I thought I'd mention it so it's on your radar as a use case. (Also this might require solving #150, so that the textual display can be produced and associated to the graphical component rather than just going on stdout.)

[favonia]

@mikeshulman Yes. The current (incomplete) design for generic locations (that generalize text ranges) is:

module type S =
sig
  type t
  val to_range : t -> Range.t option
  val pp : Format.formatter -> t -> unit
end

It's compatible with having both kinds of information or just one of them.