reduce v eval

Stream: general

[Kevin Buzzard]

I never use #reduce or #eval but I'm about to do a demo in front of a bunch of computer scientists and I noticed this:

namespace KCL -- so as not to clash with `List` in root namespace

inductive List (α : Type)
| nil : List α
| cons (a : α) (L : List α) : List α

namespace List

def L : List Nat := cons 2 (cons 37 nil)

#reduce L -- cons 2 (cons 37 nil)
#eval L -- KCL.List.cons 2 (KCL.List.cons 37 (KCL.List.nil))

I was surprised the results were different (and this is somehow confusing). Does #eval not care about namespaces but #reduce does for some reason?

[Eric Wieser]

The main difference here is that #reduce is printing an interactive expression, but #eval is printing a string

[Kyle Miller]

Add a deriving Lean.ToExpr, and they have the same output:

import Lean

namespace KCL -- so as not to clash with `List` in root namespace

inductive List (α : Type)
| nil : List α
| cons (a : α) (L : List α) : List α
deriving Lean.ToExpr

namespace List

def L : List Nat := cons 2 (cons 37 nil)

#reduce L -- cons 2 (cons 37 nil)
#eval L -- cons 2 (cons 37 nil)

[Arthur Paulino]

Oh wow, I didn't know Lean.ToExpr was a deriving handle. This is amazingly useful!
cc @John Burnham

[Kyle Miller]

(Thanks to @Alex Keizer for his work to get this into Lean core!)

[Kyle Miller]

Currently, the reason #eval L worked is that #eval can auto-derive a Repr instance. That frees you from needing to add deriving Repr for a one-off #eval.

I was thinking of having #eval be able to auto-derive a ToExpr instances as well. I haven't been completely sure whether it would be surprising to use an auto-derived ToExpr instance over a user-defined Repr instance. (I'm sure that there will be a question down the line of "why isn't my Repr instance being used here?")

[Mario Carneiro]

isn't a possible solution to that to prefer to use a Repr instance if one can be found, and only then try auto-deriving ToExpr and Repr?

[Kyle Miller]

Yeah, that's a possible solution and is under consideration too. That also has the issue where people ask "why isn't this #eval output hoverable?" or "why does this #eval give different-looking output from #reduce" (I'm less inclined to worry about this last question because of how different the evaluation models are)

Another thing to throw in is that it would be nice if #eval would add in instances for types that have no representation, with a hover explaining why not (maybe it's a function type) or what instances are missing. There's also the possibility of having recursive derivation too.

[Mario Carneiro]

ideally hoverable #eval output should be addressed by having an even more rich text format class being preferred if available, I guess ToMessageData is the relevant one in this case

[Mario Carneiro]

maybe it should even be possible to evaluate to a widget, so we can be like mathematica
image.png

[Kevin Buzzard]

I daren't ask what kind of graph product sends two graphs with three vertices to a graph with six vertices...

[Kyle Miller]

I think there's a planar immersion failure here...

[Kyle Miller]

To get something mathematica-like, one approach could be to have a separate Syntax formatting path that outputs something richer. Syntax is basically what Mathematica operates on anyway, so it has to be possible to make a "StandardForm" formatter that outputs widgets, maybe in conjunction with some delaborator configuration option to make sure the output Syntax is formattable. (I know this is sort of hacky, but this would let us take advantage of the pre-existing core delaborators.)