ToExpr, the infoview, and lcUnreachable

Stream: lean4

[Eric Wieser]

Is it reasonable for ToExpr to produce lcUnreachable terms for expressions which can only partially be reconstructed? Now that #eval tries to convert things back to expressions for the infoview, there is an incentive to producea partial conversion over no conversion at all.

[Eric Wieser]

The case I have in mind is:

open Lean Qq in
/-- Produces an arbitrary representation of the form `mₒ ⊗ₜ n₀ + ...`.

This is only for use in the infoview; it produces expressions containing `lcUnreachable`. ! -/
unsafe instance [ToLevel.{u_1}] [ToLevel.{u_5}] [ToLevel.{u_6}] [ToExpr R] [ToExpr M] [ToExpr N] :
    ToExpr (M ⊗[R] N) :=
  have eM := toTypeExprQ.{u_5} M
  have eN := toTypeExprQ.{u_6} N
  have eR := toTypeExprQ.{u_1} R
  -- we have no mechanism to obtain these instances, so just insert unreachables
  have : Q(CommSemiring $eR) := q(lcUnreachable)
  have : Q(AddCommMonoid $eM) := q(lcUnreachable)
  have : Q(AddCommMonoid $eN) := q(lcUnreachable)
  have : Q(Module $eR $eM) := q(lcUnreachable)
  have : Q(Module $eR $eN) := q(lcUnreachable)
  let single (mn : M × N) : Q($eM ⊗[$eR] $eN) :=
    let em : Q($eM) := Lean.toExpr mn.1
    let en : Q($eN) := Lean.toExpr mn.2
    q($em ⊗ₜ $en)
  { toTypeExpr := q($eM ⊗[$eR] $eN)
    toExpr mn := show Q($eM ⊗[$eR] $eN) from
      match mn.unquot with
      | [] => q(0)
      | x :: xs => xs.foldl (fun acc x => q($acc + $(single x))) (single x) }

where lcUnreachable is being used in place of typeclass instances.

[Eric Wieser]

I suppose another option would be to insert Expr.fvars or similar, but there is no NameGenerator around.

[Aaron Liu]

It's not unreachable though?

[Aaron Liu]

This one is a bit tricky

[Aaron Liu]

I guess it only works if you don't try to evaluate the expression again

[Eric Wieser]

I guess I could use sorry too?

[Eric Wieser]

A little more concretely, here's a mathlib-free example:

import Qq

universe u
open Lean Qq

structure NonemptyInterval (α : Type u) [LE α] extends Prod α α where
  /-- The starting point of an interval is smaller than the endpoint. -/
  fst_le_snd : fst ≤ snd

@[irreducible] def toTypeExprQ (α : Type u) [ToLevel.{u}] [ToExpr α] :
    Q(Type $(toLevel.{u})) :=
  toTypeExpr α

instance {α : Type u} [ToLevel.{u}] [ToExpr α] [LE α] : ToExpr (NonemptyInterval α) :=
  have eα := toTypeExprQ.{u} α
  have : Q(LE $eα) := q(lcUnreachable)
  { toTypeExpr := q(NonemptyInterval $eα)
    toExpr x := show Q(NonemptyInterval $eα) from
      have x' : Q($eα × $eα) := toExpr x.1
      q(.mk $x' lcProof) }

-- this works!
#eval NonemptyInterval.mk (1, 2) (by grind)

[Eric Wieser]

Is this use of lcUnreachable sane? Is there a better option?

[Eric Wieser]

I'll ping @Kyle Miller since I think the ToExpr in #eval was your (great!) feature

[Kyle Miller]

I wonder if there should be a namespace you could put these sorts of instances into, scoped, so that #eval can activate them?

[Eric Wieser]

Is there any harm in them being global?

[Eric Wieser]

(but if the answer is yes, indeed that sounds like a nice idea)

[Eric Wieser]

Eric Wieser said:

I suppose another option would be to insert Expr.fvars or similar, but there is no NameGenerator around.

An extreme version of this would be to move ToExpr into MetaM so that it can allocate synthetic metavariables

[Kyle Miller]

Having "fake" ToExpr instances means you can't know if the result is truly reflecting the original value, which is it's main purpose.

Another idea would be to have a parallel ToExprForPP class that could hook into ToExpr somehow — maybe by adding a local instance that bridges the two?

[Kyle Miller]

There could also be a version of this that creates Syntax directly in some sort of Delab-like monad, with ToExpr being the base case (that's not great though, since you'd want it to be able to make use of these Delab instances for subexpressions).

[Eric Wieser]

Kyle Miller said:

Another idea would be to have a parallel ToExprForPP class that could hook into ToExpr somehow — maybe by adding a local instance that bridges the two?

This sounds impractical to me, since printing List (MyUnreflectableType) is going to make code duplication for List

[Eric Wieser]

Maybe Lean.ToExpr T could become Lean.ToExpr T (lossy := false), and then the pp one would set lossy : Bool to true

[Eric Wieser]

So the container instances could just propagate the boolean unmodified

[Kyle Miller]

What's the impracticality? I'd have thought that with

class ToExprForPP (α : Type) where ...

@[priority high]
instance [ToExpr α] : ToExprForPP α where ...

def instOfToExprForPP [ToExprForPP α] : ToExpr α where ...

then #eval could add instOfToExprForPP as a local instance when synthesizing a way to pretty print the result.

[Eric Wieser]

It feels like a wart that ToExprForPP (List MyUnreflectableType) won't synthesize without the local instance

[Kyle Miller]

(deleted)

[Eric Wieser]

Though I guess you could just write

instance [ToExprForPP α] : ToExprForPP (List α) :=
  let : ToExpr α := instOfToExprForPP
  inferInstance

[Kyle Miller]

I don't think you'd ever have anything take ToExprForPP instances, just ToExpr. The only place ToExprForPP would need to appear is after the colon in the instance being defined.

[Eric Wieser]

Loogle says there are 9 instances matching Lean.ToExpr _ → Lean.ToExpr _, so adding such shortcuts by hand doesn't seem too bad

[Kyle Miller]

Why would we be adding these shortcuts?

[Eric Wieser]

I'm thinking about an end user writing #synth ToExprForPP (NotReflectable × List NotReflectable) or similar to check that they set up their instances correcty, but it not working without instOfToExprForPP being scoped

[Eric Wieser]

It's a little weird to have a typeclass whose useful instances aren't discoverable without opening a scope

[Eric Wieser]

Spelled out a bit more explicitly:

import Lean

open Lean

section InCore

class ToExprForPP (α : Type) where

instance (priority := high) [ToExpr α] : ToExprForPP α where

namespace PP
scoped instance instOfToExprForPP [ToExprForPP α] : ToExpr α := sorry
end PP

end InCore

section UserCode

structure NotReflectable where

instance : ToExprForPP NotReflectable := sorry

open PP in #synth ToExprForPP (List NotReflectable)  -- works
open PP in #synth ToExpr (List NotReflectable)  -- works, but should fail

#synth ToExprForPP (List NotReflectable)  -- this should work too
#synth ToExpr (List NotReflectable) -- fails, as desired

instance [ToExprForPP α] : ToExprForPP (List α) :=
  let : ToExpr α := PP.instOfToExprForPP
  inferInstance

#synth ToExprForPP (List NotReflectable)  -- now works without the `open`
#synth ToExpr (List NotReflectable) -- still fails, as desired

[Eric Wieser]

I think I claim that without the ToExprForPP (List α) instance this approach offers little over just declaring a preferred scope and telling users to put things in it

[Kyle Miller]

Making ToExprForPP work without enabling the scoped instance seems rather low priority to me. You're proposing that every downstream parameterized type needs to make a ToExprForPP instance too, right? That seems to be rather unfriendly.

(Can we avoid the "just" word? If ToExprForPP offers little over "just" declaring a preferred scope, then you're saying they are just about equivalent, right? Then what basis are you comparing them against to say "just"? I am assuming you're saying "using a scoped namespace avoids needing a separate class", but it's worth spelling out exactly how you are evaluating this.)

One possible reason to prefer a local instance to hook in these "partial" ToExpr instances: there's only a single instance that needs to be activated, rather than temporarily activating arbitrary number of instances. That's O(1) vs O(n).

[Eric Wieser]

Oh, I had forgotten that open scoped was O(n) !

[Kyle Miller]

This all said, I wish there were a better system for pretty printing #eval results. The autoderiving of ToExpr instances is not currently recursive (and it doesn't help you debug which ToExpr instances are missing), and there's no way to include arbitrary syntax, except by creating dummy Exprs that have custom pretty printers.

[Eric Wieser]

Kyle Miller said:

and there's no way to include arbitrary syntax, except by creating dummy Exprs that have custom pretty printers.

This somewhat feels like a feature to me, as it helps enforce that the Exprs are actually well-formed!

[Eric Wieser]

Eric Wieser said:

Maybe Lean.ToExpr T could become Lean.ToExpr T (lossy := false), and then the pp one would set lossy : Bool to true

I tried an implementation of this, which works though is perhaps a confusing interface

import Lean

section InCore

-- replace `ToExpr`
class ToExpr (α : Type) (ppOnly : Bool := false) where

abbrev ToExprForPP (α : Type) := ToExpr α (ppOnly := true)

/-- Any perfcet instance is accepted when a ppOnly one would suffice -/
instance ToExpr.forPP [ToExpr α] : ToExprForPP α := sorry

instance : ToExpr Nat := sorry

-- instances for parameterized types can propagate the `ppOnly` instance
instance [ToExpr α ppOnly] : ToExpr (List α) ppOnly := sorry
instance [ToExpr α ppOnly] [ToExpr β ppOnly] : ToExpr (α × β) ppOnly := sorry

end InCore

section UserCode

structure NotReflectable where

instance : ToExprForPP NotReflectable := sorry

#synth ToExprForPP (List NotReflectable) -- works
#synth ToExpr (List Nat)  -- works
#synth ToExpr (List NotReflectable)  -- fails, as intended


#synth ToExprForPP (List NotReflectable × Nat) -- works

but without some worse typeclass hacks the Prod instance is not well-behaved

[Eric Wieser]

Edited to match your proposed names

[Eric Wieser]

Kyle Miller said:

The autoderiving of ToExpr instances is not currently recursive

Oh, so you mean it doesn't add [ToExpr _] assumptions to the instance?

[Kyle Miller]

It adds those, definitely. The problem is that if you for example have a List MyType it won't auto-derive the ToExpr MyType instance.

[Eric Wieser]

Taking a step back, do you think it would be reasonable to add the unscoped ToExpr instances to mathlib if labelled with a Lean RFC of some kind?

[Kyle Miller]

Maybe instead of lcUnreachable you should use sorry, and maybe you could use an unsafe instance for this for the time being, to prevent it from accidentally being used in normal code?

#eval does work with unsafe instances:

structure Baz

unsafe instance : ToExpr Baz where
  toExpr _ := mkConst ``sorryAx [levelOne]
  toTypeExpr := mkConst ``Baz []

#eval Baz.mk

Rationale for avoiding lcUnreachable: if it ever slips into some actual expressions, evaluating it is undefined behavior, and also the compiler reasons about it in optimizations.

[Robin Arnez]

Another idea would be a type class like

set_option checkBinderAnnotations false in
class Lean.ToInstanceExpr (α : Type u) [α] where
  toInstanceExpr : Expr

although that means a lot of instances to make