Stream: Coq users

Topic: ✔ Proof monad?


view this post on Zulip Ignat Insarov (Oct 02 2021 at 11:07):

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Oct 02 2021 at 11:24):

the monad is implicit, it combines state and backtracking

view this post on Zulip Ignat Insarov (Oct 02 2021 at 11:29):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Oct 02 2021 at 12:10):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Théo Zimmermann (Oct 02 2021 at 12:15):

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

view this post on Zulip Enrico Tassi (Oct 02 2021 at 12:16):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Oct 02 2021 at 12:30):

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

view this post on Zulip 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.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 12:35):

All the while seemingly bringing in type safety and clarity.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Ignat Insarov (Oct 02 2021 at 12:36):

I shall provide that shortly.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Oct 02 2021 at 12:38):

y

view this post on Zulip 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.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 13:07):

@Gaëtan Gilbert   Does this example clarify anything?

view this post on Zulip Gaëtan Gilbert (Oct 02 2021 at 13:09):

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

view this post on Zulip 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?

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Oct 02 2021 at 13:12):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 13:59):

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

view this post on Zulip 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.

view this post on Zulip 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».

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 14:05):

I'm aware of desugarings.

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 14:05):

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

view this post on Zulip Ignat Insarov (Oct 02 2021 at 14:09):

I appreciate your feedback 100%.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 14:10):

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

view this post on Zulip Ignat Insarov (Oct 02 2021 at 14:11):

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

view this post on Zulip 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.

view this post on Zulip 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.

  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 ( ).

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 14:13):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 14:15):

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

view this post on Zulip Ignat Insarov (Oct 02 2021 at 14:16):

I see, I see.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 14:25):

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

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.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 14:27):

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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 14:28):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ignat Insarov (Oct 02 2021 at 14:29):

Pierre does not say that it is explicit nor implicit.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 14:30):

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

view this post on Zulip 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.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 14:30):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ignat Insarov (Oct 02 2021 at 14:34):

Concisely explained.

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Oct 02 2021 at 14:35):

I retract "pretty implicit" then.

view this post on Zulip 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).

view this post on Zulip Ignat Insarov (Oct 02 2021 at 14:37):

Fair!

view this post on Zulip 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.

view this post on Zulip Notification Bot (Oct 02 2021 at 14:43):

Ignat Insarov has marked this topic as resolved.

view this post on Zulip Ignat Insarov (Oct 04 2021 at 09:29):

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

view this post on Zulip 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 α.

view this post on Zulip 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).

view this post on Zulip Alexander Gryzlov (Oct 04 2021 at 09:50):

Idris also has an Elab monad.

view this post on Zulip 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: Mar 28 2024 at 23:01 UTC