Lean interfaces to plotting libraries?

Stream: Natural sciences

[mars0i]

I'm wondering whether anyone is working with a Lean interface to a plotting library, other than what's currently available in ProofWidgets4.

(ProofWidgets4 provides an interface to some plots in Recharts, but it's a pain to overlay multiple plots using Recharts. ProofWidgets4 also provides examples using the some of the D3 functions from Observable, but at present doesn't provide an interface to Observable's Plot library which is layered on top of D3.)

[Anand Rao Tadipatri]

I once tried interfacing with the Plotly.js library:
https://github.com/0art0/ProofWidgets4/blob/main/ProofWidgets/Component/Plotly.lean
https://github.com/0art0/ProofWidgets4/blob/main/ProofWidgets/Demos/Plotly.lean

[mars0i]

Thanks @Anand Rao Tadipatri. That might be helpful.

[Siddhartha Gadgil]

@Anand Rao Tadipatri if this is maintained it may be more useful to have this not on a fork of ProofWidgets4, so it can be used as a dependency.

[mars0i]

In the abstract it makes intuitive sense to me to have a Lean interface to a plotting library (Plotly, Observable Plot, Vega-lite, others) that is not part of ProofWidgets4, but I don't know the tradeoffs involved. I have only used ProofWidgets4 at all because that's where some existing plot functionality is available. Since I'm not a proper user of ProofWidgets--I don't really know why I would want to use it--I don't know why it might be a good thing to have a plot interface built in to it.

[Anand Rao Tadipatri]

Thanks for the suggestion. I tried putting it in a separate repository but I'm running into TypeScript build issues, likely due to improper configuration files. I'll try to see if I can compile the JavaScript file independently and put that up in the repository.

[Siddhartha Gadgil]

mars0i said:

In the abstract it makes intuitive sense to me to have a Lean interface to a plotting library (Plotly, Observable Plot, Vega-lite, others) that is not part of ProofWidgets4, but I don't know the tradeoffs involved. I have only used ProofWidgets4 at all because that's where some existing plot functionality is available. Since I'm not a proper user of ProofWidgets--I don't really know why I would want to use it--I don't know why it might be a good thing to have a plot interface built in to it.

If it were merged into ProofWidgets that would be fine. But that depends on the maintainers of ProofWidgets being happy with its current state, and also someone able to maintain if it breaks with future changes in Lean.

Otherwise, since most projects have an indirect dependency on ProofWidgets via Mathlib, also depending on a fork of it is likely to be a mess.

[Adomas Baliuka]

I wonder if it would be worth it to make a plotting library based on interval arithmetic (like Coq has one. They use GnuPlot, which I wouldn't, but a different choice seems equally possible). One could maybe even start from https://github.com/girving/interval

[Dominic Steinitz]

Having spent 20 years plotting data from Haskell (which does have a reasonable plotting library), I now just export the data as CSV and get R (ggplot) to do it. You don't have to know anything about R: ChatGPT or equivalent will do it for you. In Haskell, I am sure one could construct a plotting library as good as ggplot but it's a lot of work. For example, you want to plot data on a map with a Peters projection then R has it and I doubt anyone is working on map projections in Haskell.

image.png

[mars0i]

Adomas Baliuka said:

I wonder if it would be worth it to make a plotting library based on interval arithmetic (like Coq has one. They use GnuPlot, which I wouldn't, but a different choice seems equally possible). One could maybe even start from https://github.com/girving/interval

This is interesting. It's not something I've thought about. I glanced at that Coq page, but I don't understand what interval arithmetic is doing in the plot at the bottom, or why it's valuable to combine interval arithmetic with plotting.

(At one point I was looking into interval arithmetic libraries in OCaml, but I realized what I needed was not interval arithmetic. I was working on a model of biological evolution that used imprecise probability, which is reminiscent of interval arithmetic, but has different goals. Plotting was an important part of that project, though.)

[mars0i]

Dominic Steinitz said:

Having spent 20 years plotting data from Haskell (which does have a reasonable plotting library), I now just export the data as CSV and get R (ggplot) to do it. You don't have to know anything about R: ChatGPT or equivalent will do it for you. In Haskell, I am sure one could construct a plotting library as good as ggplot but it's a lot of work. For example, you want to plot data on a map with a Peters projection then R has it and I doubt anyone is working on map projections in Haskell.

image.png

I've used that strategy too (with a different source language), and it's great for some projects. However, I often use plotting to explore implications of varying assumptions in the math represented by my code. In that context, it's very helpful to modify the code and then immediately have a new plot appear, and then maybe change the code and do it again.

I've done this a lot in Clojure in recent years with interfaces to the Vega-lite plotting library.

It occurs to me now that it's more challenging to build an interface to, say, a Javascript plot library if you want to preserve type safety in Lean code. It seems that that means that you in effect have to duplicate everything in the plot library that's handled by strings representing options. If the library is large (like Vega-lite), this is a huge project. If one is willing to pass strings over to the Javascript plotting library, it's easier to write an interface in Lean, but then interacting with the Javascript library is less Lean-ey, and more error-prone.

[Adomas Baliuka]

mars0i said:

I glanced at that Coq page, but I don't understand what interval arithmetic is doing in the plot at the bottom, or why it's valuable to combine interval arithmetic with plotting.

The idea is that you can be "certain" the image correctly represents numerical uncertainties in calculating the function.

Of course, it's very rare that you plot functions where a "standard" plot might fool you (think e.g. aliasing if the grid is too course), so I guess the main reason why people did this was that they had the interval arithmetic already and it was a fun addition. On the other hand, it also seems in spirit of a proof assistent to have it "never fool you with a plot"