Writing UI logic in Lean

[Vtec234]

In the original ProofWidgets for Lean 3, it is possible to write user interface logic in Lean. This becomes important for users who already have large libraries of Lean code that they would like to leverage for visualization. This issue is to record how that might look in ProofWidgets4.

In React, a user interface component is a JavaScript function. In TypeScript, this function has type (props: Props) => React.ReactNode. Importantly, it may register various event handlers that react to events such as mouse clicks, or changes to the props. In a pure language such as Lean, the type of a component has to somehow account for these effects; it could be an init/view/update model as in the original ProofWidgets, or some kind of ComponentM monad. Regardless of the Lean type, the main issue is how to enable the infoview (which, recall, is an entirely separate program from the Lean server in which #eval statements and tactics execute; the infoview may invoke methods on the Lean server and access data stored there using RPC) to run this UI logic which initially only exists in Lean.

One approach is to carry out all event handling on the server. For pure components (that is ones which are stateless and register no event handlers, although there may be stateful/eventful children in their output ReactNode tree) we can do this fairly easily with a macro which expands a function MyComponent: Props → IO Html into the code block

@[server_rpc_method]
def MyComponent._rpc (p : Props) : RequestM (RequestTask Html) :=
  RequestM.asTask (MyComponent p)

@[widget_module]
def MyComponent._component : Component Props where
  -- Code to invoke `MyComponent._rpc` whenever the client-side props change,
  -- and then render the output HTML.
  javascript := (...)

With more work—some way to specify event handling, and a mechanism to pass server-side state around—this approach could be turned into a reimplementation of Lean 3-style ProofWidgets. Unfortunately, one of the core reasons for moving logic into the client was that this implementation has an intrinsically high minimal latency, as every UI event needs to roundtrip between the infoview and the Lean server (which can be on different machines). However, for many use cases this may be perfectly fine and would be worth trying.

In the ideal world, instead of running server-side, we'd have a way to compile the Lean code specifying UI logic into something that can run in the infoview. Perhaps the recent effort on LLVM could help here by allowing us to leverage LLVM's WebAssembly backend. Someone would still need to port Lean's runtime to the web, likely a full-time month's effort at least.

Short of that, it is possible to explore points along the spectrum from everything running in the server to everything running in the client. Given sufficiently general client-side code, there is room for customizing what exactly ends up being displayed just by changing RPC methods, meaning the UI can be prototyped in pure Lean. This is illustrated in InteractiveSvg. A disadvantage of this approach is that it still incurs latency, still requires writing JavaScript, and thinking about the server-client interactions can get complicated quickly.

[Vtec234]

a macro which expands a function MyComponent: Props → IO Html into the code block

Note: the mk_rpc_widget% macro now exists as of d39b9dd and release v0.0.15.

[0art0]

React supports an alternative way of specifying state update logic through Reducers.

Instead of running arbitrary JavaScript code when an event - like onClick or onHover - occurs, reducers allow UI components to dispatch a JSON-encoded message to a function called a reducer, which then handles the update logic. While the reducer is usually a JavaScript function, it may be possible to instead make it a Lean function that is called by a JavaScript function via RPC.

Reducers may allow a convenient way of defining stateful React components entirely in Lean.