Allow expression evaluation in files similar to Lean4's #eval

[michaelmesser]

• [x] I have read CONTRIBUTING.md.
• [x] I have checked that there is no existing PR/issue about my proposal.

Summary

In a Lean file

#eval 2 + 2

displays 4.

It would be nice if Idris had something similar.

Motivation

Using a REPL requires manually loading the file and running the expression on every change. This would allow continuous automatic feedback. This design is stateless which makes reasoning about it easier.

The proposal

#eval would evaluate the expression that follows

Example

In a .idr file

%eval 2 + 2

would allow something like = 4 would be displayed in the editor after the expression.

Technical implementation

A field with PosMap (NonEmptyFC, DocIdris Ann) could be added to Metadata. I'm not sure what the type of the result should be. Potentially REPLResult or something else would be better.

While traversing the definitions in a file, these evaluations would be computed and the results would be stored in the PosMap.

Alternatives considered

• REPL
  • Requires manual loading and evaluating when chance occur
  • Annoying switching of focus between file and REPL
  • Has state
• HLS like evaluation in multiline comment
  • Requires explicit click to run
  • Running a REPL in a multiline command is odd
• Jupyter notebooks
  • Overkill for many uses cases
  • Click to run introduces complex state since already run cells can be edited

Potential Extensions

If this is positively received, I may extend it to replicate other REPL functionality directly in a file. Also, perhaps clicking on the result could turn in to an assertion. Something like %eval 2 + 2 to %asserteval (2 + 2) = 4, but I haven't thought much about that yet.

Conclusion

I'm not certain if this is the best approach, but I have been unable to think of anything better.

Related Issue on the LSP: https://github.com/idris-community/idris2-lsp/issues/129

[gallais]

Isn't %asserteval just a Refl proof?

[michaelmesser]

I think so, but it would only require one line instead of two and would not require a name. Perhaps elaborator reflection would be a better way to achieve that.

[ohad]

The IDE protocol supports a message for normalising a term. Can this proposed feature be reduced to normalise term (which isn't yet implemented in idris2)?

[michaelmesser]

It has similar functionality to normalize term. I suppose it could be implemented in comments without Idris2 support.

--%eval 2 + 2

and LSP independently parse the file to find --% commands (does the Idris API expose comments or would LSP have to parse them on its own?) and Idris API functions to evaluate them.

However, this would complicate showing errors, semantic highlighting, and hover on the contents of the input.

[buzden]

It looks like %runElab logMsg "" 0 $ show $ 2 + 2 does exactly what you want except for additional logging-related printing.

You can consider addition of a function like print : Show a => a -> m Unit to the Elaboration interface and then expression %runElab print $ 2 + 2 would do what you want from %eval 2 + 2 mostly reusing what's already in the compiler.

[mattpolzin]

If you can %runElab $ print … then can’t you make print (or whatever you want to name the function) into a macro and get exactly the syntax %print …? Never done it before, but thought I saw a test case that did something like this once.

[michaelmesser]

@mattpolzin Not that I know of. As far as I know %marco f will expand f to %runElab f in an expression, but not at the top level.

[michaelmesser]

@buzden close but not quite

• I don't think the results of log messages are exposed the LSP
• This doesn't include the location of the message
• The log messages don't appear if a TTC already exists
• I'm not sure that users would want all logMsg to show up inline in their editor
• This would require users to enable elaborator reflection

[gallais]

I think so, but it would only require one line instead of two and would not require a name.

In Agda it's legal to name a throwaway toplevel definition _ precisely so that you can write tests without polluting the scope. I'd rather add this principled thing than a new pragma. The one line vs. two is moot as it's legal to write ; _ = Refl at the end.

Can this proposed feature be reduced to normalise term (which isn't yet implemented in idris2)?

Is it not? If I type an expression in the REPL it'll be evaluated.

[michaelmesser]

In Agda it's legal to name a throwaway toplevel definition _ precisely so that you can write tests without polluting the scope. I'd rather add this principled thing than a new pragma. The one line vs. two is moot as it's legal to write ; _ = Refl at the end.

%asserteval is probably not needed then.

Is it not? If I type an expression in the REPL it'll be evaluated.

%eval is intended have the same behavior as evaluating an expression at the REPL, but the interface would be very different. Are you saying %eval isn't needed at all? Or, that I should do --%eval and have LSP call normalize term on the expression? Or something else?

[gallais]

Are you saying %eval isn't needed at all? Or, that I should do --%eval and have LSP call normalize term on the expression? Or something else?

I don't like that it's a top-level pragma. That feels unprincipled: surely there are cases where I'd like to evaluate in a context?

Now that @ohad has clarified (privately) what he means by normalising an expression (essentially: automatically replacing a span of code in the source file with what it normalises to), I can see a design: some kind of open+close span tokens that delimit a subexpression & provokes the compiler to generate extra metadata annotations associated to that span.

e.g. using (| and |) as the opening & closing tokens for the sake of argument

test : (n : Nat) -> 3 + n === (| 3 + n |)
test n = Refl

would mean that on top of syntax highlighting messages stating that:

• test is a function
• Nat and (===) are type constructors
• 3 and Refl are data constructors
• n is a bound variable of type Nat

we would also get some metadata telling us 3 + n at location so-and-so reduces to S (S (S n)). The client can then decide to replace the expression by its normal form, display it in a bubble or whatever else it wants.

You should then be able to define e.g.

data Eval : a -> Type where

and write your top-level evaluation tests as

_ : Eval (| 2 + 2 |)

[michaelmesser]

I don't like that it's a top-level pragma. That feels unprincipled: surely there are cases where I'd like to evaluate in a context?

I guess my original plan for evaluate in context would be to have the user select text and trigger an evaluate in context action. I'm still trying to decide if your idea is better. Can you describe a situation where evaluating in a context would be useful?

[ohad]

One example comes up in @madman-bob 's work on tabular data.

We have operations on tabular data that change the schema:

result : Table ?hole
result = join students grades ["name", "age"]

and when you search/refine hole you get:

result : Table ([< "name" :! String, "age" :! Nat, "matriculation year" :! Nat] ++ [< "name" :! String, "age" :! Nat, "linear algebra 1" :< Nat, "introduction to programming with Idris" :< Nat] |-| ["name", "age"])
result = join students grades ["name", "age"]

Which you'd then want to normalise into:

result : Table ([< "name" :! String, "age" :! Nat, "matriculation year" :! Nat, "linear algebra 1" :< Nat, "introduction to programming with Idris" :< Nat])

[michaelmesser]

Based on that use case, I feel my select and action idea would make the most sense for evaluating in a context. Is there a case where you would want continuous feedback on evaluating in a context like I am proposing with %eval?