Stream: Coq users

Topic: ✔ Proof monad?

Ignat Insarov (Oct 02 2021 at 11:07):

• Proof state is a state, and tactics are actions that act on it. This looks like there should be a monad here. Is there?
• Introducing something like do notation of Haskell seems like it could have made the design of a tactics language simpler. Has it been considered?

Ignat Insarov (Oct 02 2021 at 11:13):

Particularly as concerns Ltac2, instead of requiring that everything be a function from the unit type, one might say that tactics are monadic actions. A key word like Proof (which currently does nothing) might then enter the special «proof mode» where Ltac2 actions can be lined up for execution.

Gaëtan Gilbert (Oct 02 2021 at 11:24):

the monad is implicit, it combines state and backtracking

Ignat Insarov (Oct 02 2021 at 11:29):

What exactly do you mean when you say «implicit»?

Paolo Giarrusso (Oct 02 2021 at 12:00):

@Ignat Insarov There isn't universal agreement that using monads "the Haskell way" is a superior solution — some people prefer Haskell, others prefer OCaml, and they have different kinds of syntactic noise due to effects.

Paolo Giarrusso (Oct 02 2021 at 12:02):

in ML-like languages, including OCaml and Ltac2, a monad exists, but it appears in the language semantics. (Historically, that's how monads were introduced into programming by Moggi, BTW — before their use in Haskell).

Paolo Giarrusso (Oct 02 2021 at 12:04):

Concretely, ML asks you to thunk actions, while Haskell requires do notation and a plethora of combinators for dealing with different kind of effects. I've used quite a bit of Haskell, but it's not a trivial overhead either.

Enrico Tassi (Oct 02 2021 at 12:10):

Yes, "implicit" means that you don't have to write bind and return explicitly.

Ignat Insarov (Oct 02 2021 at 12:10):

Correct me if I am wrong, but the situation is that OCaml explicitly wants to ignore effects on the type level, while Haskell wants to track effects on the type level. So, in OCaml effectful values by themselves are not marked and the programmer has to convert them to trivial functions from the unit type if they wish to withhold from executing them, while in Haskell effectful values are already marked on the type level with a monadic functor.

Ignat Insarov (Oct 02 2021 at 12:12):

So it seems to me that, insofar as we want to track the effects of tactics, the monadic functor in their type is the way to go.

Enrico Tassi (Oct 02 2021 at 12:12):

The thunk part is just to let one chose "when" things happens, it is not necessarily a "tag" to say that something is effectful (it does not tell you which effect is performed for example)

Théo Zimmermann (Oct 02 2021 at 12:15):

You may want to delay a computation for performance reasons too.

Enrico Tassi (Oct 02 2021 at 12:16):

This is the "selling argument" about haskell I never really bought ;-)

Enrico Tassi (Oct 02 2021 at 12:18):

I know @Pierre-Marie Pédrot managed to pull out some perf by "thunking" here and there, IIRC in the detyping code. But one could also argue that the code is not exactly doing what one should (traversing a term that the next phase is telling you to ignore... IMO the pipeline is chopped wrongly)

Théo Zimmermann (Oct 02 2021 at 12:19):

You can do that pretty easily in OCaml. I was trying to give an example of why you may put a thunk into something that doesn't do effectful computations.

Ignat Insarov (Oct 02 2021 at 12:28):

I am not sure I follow the conversation. What I said is that the accepted requirements of proof writing («… a language featuring notation facilities to help write palatable scripts …») seem to be better addressed by making tactics monadic actions, marked at the type level by a monadic functor. A key word similar to «Proof» could serve to indicate that the ensuing series of actions is to be executed with the initial state given by the statement of the theorem.

Ignat Insarov (Oct 02 2021 at 12:29):

This is not an argument about Haskell abstractly, but rather an argument that the way Haskell offers to work with actions is suited to the task of writing beautiful proof scripts.

Gaëtan Gilbert (Oct 02 2021 at 12:30):

when everything is in the monad, why not make the monad implicit?

Ignat Insarov (Oct 02 2021 at 12:34):

I should ask you again to say precisely what you mean by «implicit». We already have the key words Proof and Qed. And Ltac2 asks us to also write a number of unit values into the proof script. The solution I am talking about does not require anything beyond Proof and Qed to delimit the monadic section.

Ignat Insarov (Oct 02 2021 at 12:35):

All the while seemingly bringing in type safety and clarity.

Gaëtan Gilbert (Oct 02 2021 at 12:35):

the monad is implicit meaning that let x := bla in bli in used syntax corresponds to a bind in the state+backtrack monad

Gaëtan Gilbert (Oct 02 2021 at 12:35):

I don't understand what you want at all, maybe it would be clearer to provide some examples in imagined syntax?

Ignat Insarov (Oct 02 2021 at 12:36):

I shall provide that shortly.

Pierre Courtieu (Oct 02 2021 at 12:37):

Is it true to say that in ocaml the proof state IS a monad. Ltac has an imperative syntax but translates to this monad.

Gaëtan Gilbert (Oct 02 2021 at 12:38):

y

Ignat Insarov (Oct 02 2021 at 13:06):

So, consider this example:

Set Default Proof Mode "Classic".

Ltac higher_order_tactic tactic := tactic.

Goal 1 + 1 = 2.
Proof.
  higher_order_tactic simpl. (* simpl: unit → unit — please do not evaluate yet! *)
  simpl. (* simpl: unit — now please evaluate! *)
  reflexivity.
Qed.

— Here, simpl was not well typed. Ltac1 lets us do it anyway because of magic.

Set Default Proof Mode "Ltac2".

Ltac2 higher_order_tactic tactic := tactic ( ).
Ltac2 dimple ( ) := simpl.

Ltac2 Eval higher_order_tactic.
Ltac2 Eval dimple.
Ltac2 Eval higher_order_tactic dimple.
Fail Ltac2 Eval higher_order_tactic (dimple ( )).

Goal 1 + 1 = 2.
Proof.
  higher_order_tactic dimple. (* This works fine. *)
  dimple. (* Warning: The following expression should have type unit. [not-unit,ltac] — no actions taken! *)
  dimple ( ). (* Now it works. *)
  reflexivity.
Qed.

— Here, Ltac2 accepts dimple and ignores it with a warning, because it is not well typed.

Now in the imaginary monadic proof system:

Set Default Proof Mode "Monadic".

Monadic higher_order_tactic tactic := tactic.
Monadic Check higher_order_tactic. (* higher_order_tactic: Tactic ( ) → Tactic ( ) *)
Monadic dimple := simpl.
Monadic Check dimple (* dimple: Tactic ( ) *)

Goal 1 + 1 = 2.
Proof. (* action block begins *)
  (* In an action block, the dot has type Tactic ( ) → Tactic ( ) → Tactic ( ) *)
  higher_order_tactic dimple. (* higher_order_tactic dimple: Tactic ( ) *)
  dimple. (* dimple: Tactic ( ) *)
  dimple ( ). (* Type error: dimple is not a function. *)
  reflexivity.
Qed. (* action block ends, action is evaluated with evaluate_tactic: Tactic ( ) → a_legit_proof_term *)

— Here, everything is well typed and yet looks exactly like Ltac1 — no need to apply dimple to anything.

Ignat Insarov (Oct 02 2021 at 13:07):

@Gaëtan Gilbert   Does this example clarify anything?

Gaëtan Gilbert (Oct 02 2021 at 13:09):

(aside: why do you put a space in your ()?)

Paolo Giarrusso (Oct 02 2021 at 13:10):

@Ignat Insarov When you say "the dot has type ...", do you actually propose to delay execution of the whole tactic script until the end? I'd assume not, but then what does that mean?

Gaëtan Gilbert (Oct 02 2021 at 13:11):

so the dot has magic? we already have enough problems with dot having magic with solve_constraints, let's not add more

action block ends, action is evaluated with evaluate_tactic

what about stepping command by command (the only sane way to use tactics)?

Ignat Insarov (Oct 02 2021 at 13:11):

Gaëtan Gilbert said:

(aside: why do you put a space in your ()?)

Parentheses with some space inside look better in variable pitch fonts than simply adjacent parentheses.

Gaëtan Gilbert (Oct 02 2021 at 13:12):

also not sure how this is different from ltac1-with-types

Paolo Giarrusso (Oct 02 2021 at 13:13):

It does not seem a complete proposal, since it doesn't show how one would define functions in do-like notation, and how one would define pure functions.

Paolo Giarrusso (Oct 02 2021 at 13:16):

however, IMHO it wouldn't that absurd if the proof mode used a different syntax from writing actual functions.

Ignat Insarov (Oct 02 2021 at 13:48):

I am not making a proposal. I am merely asking a question. Does this approach make sense? Has it been tried?

Ignat Insarov (Oct 02 2021 at 13:57):

Gaëtan Gilbert said:

so the dot has magic? we already have enough problems with dot having magic with solve_constraints, let's not add more

The dot is already a key word, it has some meaning to a compiler or interpreter. I do not see what makes one meaning magical and another mundane.

Paolo Giarrusso (Oct 02 2021 at 13:58):

if the . is simply an operator with the type you give, then it's _not_ magical, but single-stepping scripts would be impossible; in that case, I'd say the approach would not make sense.

Paolo Giarrusso (Oct 02 2021 at 13:59):

OTOH, I'm sure there's some way to write a monadic tactic language!

Paolo Giarrusso (Oct 02 2021 at 14:03):

But it's not clear why one would, and your example is not developed enough to clarify that.

If all you want is avoid the noise from ( ), I think all you'd need is a shorter syntax to wrap Ltac2 functions into tactic notations.

Ignat Insarov (Oct 02 2021 at 14:03):

Yo, the dot does not need to have a type and needs not be a value itself. For example, in Haskell the line break is a special token, but it invokes the composition of monadic actions under the hood when that is dictated by context. (Syntactic context. This happens before type checking even.) That is to say, Haskell substitutes the composition of actions in the right places. This is called «syntactic desugaring».

Paolo Giarrusso (Oct 02 2021 at 14:05):

I'm aware of desugarings.

Paolo Giarrusso (Oct 02 2021 at 14:05):

Your comment describe a possible design, I gave feedback to that.

Ignat Insarov (Oct 02 2021 at 14:09):

I appreciate your feedback 100%.

Paolo Giarrusso (Oct 02 2021 at 14:09):

I guess the best answer is as follows: different "sentences" in proof scripts are not composed monadically.

Paolo Giarrusso (Oct 02 2021 at 14:10):

sentences = the dot-separated parts. Each is executed separately, then control returns to the user.

Ignat Insarov (Oct 02 2021 at 14:11):

Yes, how this translates to interactive proof writing is the right question to ask.

Ignat Insarov (Oct 02 2021 at 14:11):

I can imagine how it would happen but I am not sure what would constitute a proof that it is legit.

Ignat Insarov (Oct 02 2021 at 14:12):

Suppose this:

1. A proof script is a sequence of sentences that describe actions — values of type Tactic ( ).
2. We send the sentence that describes the first action to Coq.

3. Coq interprets it as a function of type Proof_State → either Proof_State or Error, puts the current state onto a stack then tries to apply the function to it.

   • If it does not apply, Coq tells us so and we must fix the sentence.
   • If it applies, Coq tells us so and informs us of the new state.
   • It is also possible that the sentence does not parse or does not type check as Tactic ( ). In this case Coq does nothing and simply tells us the syntax or type error.

4. If we are stuck, we may ask Coq to take the previous state from the stack and try another way. This is a special, hard-coded language primitive undo: Tactic ( ).

Paolo Giarrusso (Oct 02 2021 at 14:13):

that makes sense, but I suspect the problem needs reframing...

Paolo Giarrusso (Oct 02 2021 at 14:13):

to me, I guess the point is that ltac1 was designed ^W nope, it grew to be convenient in proof blocks, but as a result it's completely unusable for nontrivial programs

Paolo Giarrusso (Oct 02 2021 at 14:14):

and we're not talking of something "high-brow" or "ivory tower" — I'd be terrified of writing a sort in ltac1.

Paolo Giarrusso (Oct 02 2021 at 14:15):

so, that's about making Ltac2 quicksort () := ... better.

Ignat Insarov (Oct 02 2021 at 14:16):

I see, I see.

Ignat Insarov (Oct 02 2021 at 14:16):

Individual values of type Tactic ( ) may be defined separately via some language. As they are today. They are going to be given to Coq as sentences, Coq is going to parse them as free monadic values and save into the context, from which they may be looked up.

That is to say, insofar as we can write free monadic expressions, we are good to go. And we know that we can because free monadic values are defined exactly as any other monadic values, and it is being done every day.

Paolo Giarrusso (Oct 02 2021 at 14:17):

... so, that doesn't mean it's the best for proof blocks, but AFAICT it seems the main problem you have complained about until now could be solved directly via other sugar...

Paolo Giarrusso (Oct 02 2021 at 14:18):

that is, _if_ the problem is the extra noise in using Ltac2 dimple ( ) := simpl., or the one in writing Ltac2 dimple ( ) := simpl. and adding a tactic notation to use dimple, there might be some syntactic sugar on top.

Ignat Insarov (Oct 02 2021 at 14:25):

We can even be more specific than «some free monad». What we need to describe is:

• How to ask what the proof state is — getting a value of type Proof_State out of thin air. So, the primitive is ask: Tactic Proof_State.
• How to take a step back — a special value step_back: Tactic ( ).

In Haskell this would mean defining a functor Base_Of_Tactic: Λα → Ask α × Step_Back then taking its free monad Tactic = Free Base_Of_Tactic. The meaning of a term of type Tactic ( ) is a function Proof_State → either Proof_State or Error that can be executed on the back end as I described above.

Ignat Insarov (Oct 02 2021 at 14:27):

I am not sure if doing this in OCaml is hard…

Paolo Giarrusso (Oct 02 2021 at 14:27):

you don't need to say more on that to convince me — we treat . like today, rather than an operator, fine. But then, still, I'm not sure what's the proposal and _why_ we need it

Paolo Giarrusso (Oct 02 2021 at 14:28):

and as others said, an explicit proof monad already exists in the implementation

Ignat Insarov (Oct 02 2021 at 14:28):

Gaëtan Gilbert said:

the monad is implicit, it combines state and backtracking

— They said the opposite.

Paolo Giarrusso (Oct 02 2021 at 14:28):

see Pierre Courtieau above https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Proof.20monad.3F/near/255868306

Ignat Insarov (Oct 02 2021 at 14:29):

Pierre does not say that it is explicit nor implicit.

Ignat Insarov (Oct 02 2021 at 14:30):

Also, that is another monad — the proof state monad.

Paolo Giarrusso (Oct 02 2021 at 14:30):

AFAICT, that's the monad that is used in Ltac (1 and 2) to sequence effects inside a sentence.

Ignat Insarov (Oct 02 2021 at 14:30):

I am not sure what it is, actually. Is it documented anywhere?

Ignat Insarov (Oct 02 2021 at 14:32):

There is something on the back end that actually stores the proof state and that tactics act upon. I would not immediately jump to the conclusion that it is the same monad as the Tactic I described.

Paolo Giarrusso (Oct 02 2021 at 14:32):

for Ltac1, it's not really documented. For Ltac2, there are some hints in the docs, but they are pretty implicit.

Ignat Insarov (Oct 02 2021 at 14:34):

So then one of the reasons I should want this is that it can be explained in widely recognized terms.

Ignat Insarov (Oct 02 2021 at 14:34):

Concisely explained.

Paolo Giarrusso (Oct 02 2021 at 14:34):

https://coq.inria.fr/refman/proof-engine/ltac2.html#effects

We recall that the Proofview.tactic monad is essentially a IO monad together with backtracking state representing the proof state.

Paolo Giarrusso (Oct 02 2021 at 14:35):

I retract "pretty implicit" then.

Paolo Giarrusso (Oct 02 2021 at 14:36):

And I'm going to dispute the idea that having in-language monads (like in Haskell) is any more "widely recognized" than having the monad in the semantics (like in usual imperative languages).

Ignat Insarov (Oct 02 2021 at 14:37):

Fair!

Ignat Insarov (Oct 02 2021 at 14:43):

So the conclusion is that the dice are cast already and it is cheaper to live with some extra parentheses, possibly remedied by some syntactic sugar, than to design yet another proof language.

Notification Bot (Oct 02 2021 at 14:43):

Ignat Insarov has marked this topic as resolved.

Ignat Insarov (Oct 04 2021 at 09:29):

Turns out what I suggested above is similar to the way Lean does things.

Ignat Insarov (Oct 04 2021 at 09:29):

The type of a function that can inspect the proof state, modify it, and potentially return something of type α (or fail) is called tactic α.

Kevin Buzzard (Oct 04 2021 at 09:34):

Lean will have the same problems as being discussed here, moving from Lean 3 to Lean 4 (Lean tactics are written in Lean and so all tactics need to be rewritten manually).

Alexander Gryzlov (Oct 04 2021 at 09:50):

Idris also has an Elab monad.

Ignat Insarov (Oct 04 2021 at 12:13):

If anyone is curious to know more, section 7.2 of The Hitchhiker’s Guide to Logical Verification talks about the tactic monad and enumerates its feature.

Last updated: Sep 23 2023 at 06:01 UTC