do
notation of Haskell seems like it could have made the design of a tactics language simpler. Has it been considered?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.
the monad is implicit, it combines state and backtracking
What exactly do you mean when you say «implicit»?
@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.
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).
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.
Yes, "implicit" means that you don't have to write bind
and return
explicitly.
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.
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.
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)
You may want to delay a computation for performance reasons too.
This is the "selling argument" about haskell I never really bought ;-)
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)
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.
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.
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.
when everything is in the monad, why not make the monad implicit?
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.
All the while seemingly bringing in type safety and clarity.
the monad is implicit meaning that let x := bla in bli
in used syntax corresponds to a bind in the state+backtrack monad
I don't understand what you want at all, maybe it would be clearer to provide some examples in imagined syntax?
I shall provide that shortly.
Is it true to say that in ocaml the proof state IS a monad. Ltac has an imperative syntax but translates to this monad.
y
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.
@Gaëtan Gilbert Does this example clarify anything?
(aside: why do you put a space in your ()
?)
@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?
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)?
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.
also not sure how this is different from ltac1-with-types
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.
however, IMHO it wouldn't that absurd if the proof mode used a different syntax from writing actual functions.
I am not making a proposal. I am merely asking a question. Does this approach make sense? Has it been tried?
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.
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.
OTOH, I'm sure there's some way to write a monadic tactic language!
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.
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».
I'm aware of desugarings.
Your comment describe a possible design, I gave feedback to that.
I appreciate your feedback 100%.
I guess the best answer is as follows: different "sentences" in proof scripts are not composed monadically.
sentences = the dot-separated parts. Each is executed separately, then control returns to the user.
Yes, how this translates to interactive proof writing is the right question to ask.
I can imagine how it would happen but I am not sure what would constitute a proof that it is legit.
Suppose this:
Tactic ( )
.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.
Tactic ( )
. In this case Coq does nothing and simply tells us the syntax or type error.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 ( )
.
that makes sense, but I suspect the problem needs reframing...
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
and we're not talking of something "high-brow" or "ivory tower" — I'd be terrified of writing a sort in ltac1.
so, that's about making Ltac2 quicksort () := ...
better.
I see, I see.
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.
... 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...
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.
We can even be more specific than «some free monad». What we need to describe is:
Proof_State
out of thin air. So, the primitive is ask: Tactic Proof_State
.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.
I am not sure if doing this in OCaml is hard…
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
and as others said, an explicit proof monad already exists in the implementation
Gaëtan Gilbert said:
the monad is implicit, it combines state and backtracking
— They said the opposite.
see Pierre Courtieau above https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Proof.20monad.3F/near/255868306
Pierre does not say that it is explicit nor implicit.
Also, that is another monad — the proof state monad.
AFAICT, that's the monad that is used in Ltac (1 and 2) to sequence effects inside a sentence.
I am not sure what it is, actually. Is it documented anywhere?
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.
for Ltac1, it's not really documented. For Ltac2, there are some hints in the docs, but they are pretty implicit.
So then one of the reasons I should want this is that it can be explained in widely recognized terms.
Concisely explained.
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.
I retract "pretty implicit" then.
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).
Fair!
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.
Ignat Insarov has marked this topic as resolved.
Turns out what I suggested above is similar to the way Lean does things.
The type of a function that can inspect the proof state, modify it, and potentially return something of type
α
(or fail) is calledtactic α
.
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).
Idris also has an Elab
monad.
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: Feb 04 2023 at 21:02 UTC