I've never seen a title that promised so much and delivered it all.
That said, I'm very glad programming is not done through tactics. Editing proofs written with tactics is a nightmare - and the main reasons it's tolerated are the ubiquity of interactive provers and the fact that you basically don't care about which particular proof you get in a prover - unlike code, which rarely has interactive typechecking (Haskell holes come close) and where you do, definitely, care about the specific code you write.
Using tactics for metaprogramming addresses all of those concerns, and it will be interesting to see if it picks up any kind of steam. Formalising the existing use of Eclipse-style code templates with a more powerful system should have loads of promise.
>Editing proofs written with tactics is a nightmare
How so? Writing proofs in Agda is a joy, but it completely fails to document what I spend most of my time looking at: The context and the subgoal. Tactics only documenting this when you're able to step through them isn't something I'd hold against them, they're intended for interactive provers after all.
Well, in part because they don't document the context and the goal. Code has a clear context (variables and functions in scope) and a clear goal (return type). Editing code vs tactics is easy because the impact that each edit has on the context, goal, and code is clear and localised. Add or remove a tactic, and the rest of the proof can be completely invalidated.
The fact that you can look at a code snippet and tell what it does, but looking at a tactic snippet essentially tells you nothing, is exemplary of the difference. Just the fact that you need a more powerful editing tool (interactive provers) to edit tactic proofs at all is testament to how much more complicated they are.
>Code has a clear context (variables and functions in scope) and a clear goal (return type).
At the top level, sure, but if you have a more complex proof term this breaks completely down. You'd have to evaluate potentially arbitrary expressions to determine the types and furthermore there is nothing to indicate the 'human' rather than mechanical structure of the proof since metavariables are just completely gone. It's just not my experience that I could look at a complex proof term (where I don't already know the underlying proof) and figure it out without using an interactive prover.
>Add or remove a tactic, and the rest of the proof can be completely invalidated
Just like if you randomly removed a part of a proof in term form it wouldn't typecheck anymore? 'stupid' tactics are just as localized as inserting the corresponding term with metavariables . If you're talking about how automation tactics are heavily context dependent, this is more of a fundamental quality of automation rather than tactics. Automation done via reflection suffers from the same issue.
Is there a more free-form version of typed holes? The implementations here seem very cumbersome. Perhaps a version of this that has more focus on the duality of code as both runnable, complete code, and intermediate form between thought and code.
I hate to be a downer, but I just don't trust automatic code generation.
Proof automation is nice because proofs are ultimately irrelevant. It doesn't matter what the proof is, only that there is one. With code, it's another matter. If I have to depend on heuristics for it to choose the right option that means that I'll actually have to read and verify whether it chose the correct one. At that point, I feel like I'm not really winning anything over just writing it myself.
It's possible to write a complex specification to ensure the generated code would be correct, but current automation already struggles with generating proofs for hand written code, let alone generating code and verifying it.
Also, it isn't clear to me whether tactics programs are supposed to be kept as code or just used by the LSP which the gif makes it seem like. To me the strongest benefits of tactics are that they can be used to document what the author was trying to do and that using an IDE they can be executed step-by-step. If it's just to be used by the LSP: What is the point of using tactics vs normal metaprogramming?
Note that these are tactics for metaprogramming - the tactics are themselves for programming, not for use in programs. The commands to the LSP tell it how to generate the code, and the code sticks around for editing afterwards.
>If it's just to be used by the LSP: What is the point of using tactics vs normal metaprogramming?
What is "normal" metaprogramming? The particular benefit of using tactics would be that they're designed for small steps of in-flight editing, rather than generating something all at once; and that their vocabulary is pretty well established.
>Note that these are tactics for metaprogramming - the tactics are themselves for programming, not for use in programs.
I don't understand what this is supposed to mean. How are e.g. coq tactics not the exact same?
>The commands to the LSP tell it how to generate the code, and the code sticks around for editing afterwards.
Not having the metaprogram which generated the code around just strikes me more as an anti-feature.
>What is "normal" metaprogramming?
Arbitrary, "non-sequential" code transformations.
>The particular benefit of using tactics would be that they're designed for small steps of in-flight editing, rather than generating something all at once
Well, for me tactics definitely invokes more serious proof automation than just what you could also do using Agda's emacs commands. This is also the impression I get from the article, the image presented uses some form of auto tactic to generate an entire term in one go. Certainly not what I'd call "small steps of in-flight editing".
>I don't understand what this is supposed to mean. How are e.g. coq tactics not the exact same?
Coq tactics are code - you write terms using tactics, and you edit the term by editing the tactics. Save and load the file, and only the tactics stick around.
In this version, tactics write code - you use tactics to generate a term (Haskell code), and then you can edit the term itself. Save and load the file, and all you get is the Haskell code: the tactics only existed for codegen.
>Not having the metaprogram which generated the code around just strikes me more as an anti-feature.
Why? The trouble with metaprogramming is that you basically never want to have the power to simultaneously edit the program and the metaprogram. As you yourself pointed out, tactics would be terrible as an opaque metaprogram - they only work if you don't care about the particular term they generate.
Tactic metaprogramming lets you write terms quickly - it fulfills a need that lots of Haskell programmers have, which is that certain type signatures have "obvious" inhabitants and actually expressing those inhabitants can itself feel like a lot of boilerplate. But since you need to edit the Haskell code itself, the metaprogram must disappear. You won't miss it, since you won't need to regenerate the program from the metaprogram.
>the image presented uses some form of auto tactic to generate an entire term in one go
Because it's built out of several tactic steps, which the article goes into the construction of. You could still (presumably) have built it piece by piece, by applying each tactic one at a time - and each step only modifies the term slightly, leaving a hole for later steps.
>In this version, tactics write code - you use tactics to generate a term (Haskell code), and then you can edit the term itself. Save and load the file, and all you get is the Haskell code: the tactics only existed for codegen.
There's nothing preventing you from already doing this. You can use Isabelle's hammer/CoqHammer to generate a proof, dump the proof term and then replace your usage of the hammer tactic with the term. It's just, why would you want to edit the proof term manually? I'm pretty sure you can do this with Haskell's normal metaprogramming facilities too, it's just really not the intended way.
>Why?
Because it's a lot harder to maintain. Not only do you lose out on information about the generation (Why/How was it generated?), if you change the code it was generated from, you'll have to either manually edit the generated code (especially troublesome because the information of how it was generated was thrown away!) or you'll have to figure out how to do it using tactics again (in that case, why not just keep the tactics as documentation?).
>As you yourself pointed out, tactics would be terrible as an opaque metaprogram - they only work if you don't care about the particular term they generate.
Tactics aren't 'opaque', it's just a pain to manually look at the generated code and I don't see how the same doesn't apply here.
>Because it's built out of several tactic steps, which the article goes into the construction of. You could still (presumably) have built it piece by piece, by applying each tactic one at a time - and each step only modifies the term slightly, leaving a hole for later steps.
You could, but it seems pretty clear to me that this is not the intention. If you just want some form of 'quick actions' you don't need a tactics system. Having an option to 'try filling this hole' heavily indicates that this is to be used for more heavy automation.
>It's just, why would you want to edit the proof term manually?
Because you want to produce a particular proof term, because you are programming, not proving. Even with the CHC, there is a distinction between the two.
>Not only do you lose out on information about the generation (Why/How was it generated?), if you change the code it was generated from, you'll have to either manually edit the generated code (especially troublesome because the information of how it was generated was thrown away!)
This is a standard part of programming. Very rarely does editing code come with the complement of how/why the code itself was written - and even it does (like through doc comments) editing the code can then invalidate that information because the motivation can become outdated.
>Tactics aren't 'opaque', it's just a pain to manually look at the generated code and I don't see how the same doesn't apply here.
Because you want to look at the code, because the generated code is the objective of writing the tactics. You are not programming with tactics, you are writing code with tactics.
The point is this: if you wanted to prove `a -> a -> a`, then `intros; assumption` is a fine proof. But if you want to define `min :: (Ord a) => a -> a -> a`, then `intros; assumption` would typecheck without doing what you want. Tactics are not a good fit for programming, in general, because they fit the very different purpose of finding inhabitants rather than specifying them.
By contrast, actually writing code does seem like a good fit for tactics, because the steps you might take to iteratively program the particular term you want fit nicely with individual tactics.
I'm not sure what you mean? The induction tactic uses the induction principle (dependent eliminator) of the corresponding type. If you unfold the dependent eliminator, it boils down to a combination of fix and match. I don't see how you could get a term simpler than that, unless you mean something else by readable?
IIRC, the match it generates often ends up being a dependent match using the convoy pattern once nontrivial functions start being written, which quickly gets really really hard to read. Maybe this is partly the fault of Coq's matching requiring the convoy pattern (unlike Agda's or Idris's), but I find it extremely difficult to read these terms, versus hand-written ones.
For the recursive functor application example on a tree, normal meta-programming would be a macro taking the type as an argument, and then generating the resulting case by case application code, at compile time.
This would be much clearer and could automatically keep working if more cases were added (adding new node types is common when adding language features to abstract syntax trees).
This is a very awesome demo but my experience with other templating systems in IDEs (like autogenerated toString and other methods in Java) is that making boilerplate easy to write doesn't help make it easier to read or modify.
I agree; the most exciting use case for a system like this would be that it would functionally (no pun intended) replace the idea of "tab-completion" for typed functional programming languages.
This is really incredible work, wonderful in fact, but at the same time it simply excites me for tools that go further.
Having to key in the correct tactic to fill in a program still involves the same actions required by typing a program as text namely thinking (identifying which tactic is the correct one) and typing (keying in the tactic). A system that “derives the obvious functor for a data type automatically”, permitting overrides would be more useful.
For most programers the ROI on learning tactics isn’t that high. It effectively entails encoding the basic things they already understand like pattern matching into more abstract jargon that, while more general, requires further study to use properly. Most of the time, especially for complex cases, it will be faster and lower effort to just write the pattern match yourself rather than have to think in terms of sequences of abstract operations and recall that “oh I need ‘homo a b’, ‘refl’ here or w/e (some might disagree, but I find thinking in terms of concrete matching on symbols is much easier than thinking in terms of sequences of tactic/proof operations, recalling what they do, etc.)
For this reason, I personally don’t think programing with theorem proving/tactics will take off until the basic derivations are entirely automatic and tuning them to a complex or custom use case is a matter of easily retyping one or two proof lines.
> For this reason, I personally don’t think programing with theorem proving/tactics will take off until the basic derivations are entirely automatic and tuning them to a complex or custom use case is a matter of easily retyping one or two proof lines.
That's what the GIF at the top of the article shows: The two choices are
1. Attempt to fill hole
2. Introduce lambda
The user types "1" and the rest happens automatically.
> just write the pattern match yourself rather than have to think in terms of sequences of abstract operations and recall that “oh I need ‘homo a b’, ‘refl’ here
The interface suggests that you won't need to recall that you need "homo"; it'll be presented as one of several possible choices and you only need to recognize that this is the choice you want (or not).
You’re right! thanks for pointing that out. I scrolled past the gif and read the article which gave the impression a lot of the work was manual since it proceeded step by step. But yes, the LSP powered suggestions seem to be exactly the kind of thing that I’d love to see.
Very nice. I am hoping for semantic editing to make it into Haskell mainstream since I saw idris-mode in action for the first time. Even if it is just a small step sometimes, watching your editor write code for you based on what is already known from types is extremely cool.
Note to the author: There is a typo in the code: fmap = \fab ma -> case eca of ... s/ma/eca/ or the other way around.
Those two programs don't use a in the Nothing case, they have Just _ instead, i.e. a hole. Those are just as valid as any other program with a hole. You could fill the hole with undefined if you wanted to.
how pragmatic is algebra driven design in the real world?
Real world are full of exceptions, and I am doubtful those can be modelled with any kind of algebra.
It's not useful in every scenario but it's useful more often than you might think and it's very effective when it is useful. The book has two great examples.
Yet another buzzword used to make Haskell sound special and out of ordinary, while really they should make it more accessible and familiar to large audiences.
If you're talking about tactics, they're a very old idea, dating back at least to Isabelle and Coq. Yes, it'd be nice to make things more accessible to a general audience, but this post isn't trying to do that.
To follow up: I believe the original paper introducing tactics is Milner's still excellent "The Use of Machines to Assist in Rigorous Proof" from 1984 [1].
The basic idea is that a "tactic" is a function which inputs some abstract goal and outputs a pair consisting of subgoals and a mechanism by which the solutions to those subgoals can be combined into a solution to the original goal. This is a very general notion, but it was mostly influential in Milner's style of theorem prover. To this day, most proofs in HOL systems such as HOL4 and HOL Light are just combinations of tactics.
That tactics could potentially be used in Haskell is just a reflection of the fact that Haskell's type system has a connection to propositional logic, where Milner's tactics become a mechanism by which to come up with a program (solution) matching a type (goal).
Edinburgh LCF already had tactics, both the book about it and the paper "A Metalanguage for Interactive Proof in LCF" from 1978 mention it and I wouldn't be surprised if there was an even earlier mention. Pretty crazy to think about how ML was devised to allow a safe working with tactics.
Oh wow! The paper [1] already introduces "tacticals", being functions from tactics to tactics that give you a very powerful language for composing tactics, and its examples are still very close to what you would see in things like HOL Light:
(REPEAT GENTAC) THEN REPEAT (ANYCASESTAC THEN SIMPTAC).
Every one of these identifiers is an ordinary ML function. "THEN" is infix.
>When you stop and think about it, that’s like the stupidest idea ever.
No, when I read the headline I immediately thought, "Why would would anyone ever want to do this?".
I once had to work with some crappy visual basic editor from Microsoft. It basically ran the compiler on every keystroke and if your code is temporarily invalid then it will open a dialog telling you your code is invalid (with no indication what is invalid or where). You know, my code might not be valid in this second but it will be in a minute. However, since every construct had to be valid until I reach my "destination" the editor forced me to think outside of it. People write out their thoughts as code so they don't have to keep them in their head. Sometimes those thoughts are not valid code but they are thoughts nevertheless.
Then there is the obvious data transmission problem. We have 10 fingers so we can easily transmit 10 bits of information per second. Try doing that with your tongue or your toes. We can have blind or deaf programmers but if you lose both your hands your career is over.
Programming is text because anything else would be stupid. Show me your semantic muscles and I'll change my mind.
That said, I'm very glad programming is not done through tactics. Editing proofs written with tactics is a nightmare - and the main reasons it's tolerated are the ubiquity of interactive provers and the fact that you basically don't care about which particular proof you get in a prover - unlike code, which rarely has interactive typechecking (Haskell holes come close) and where you do, definitely, care about the specific code you write.
Using tactics for metaprogramming addresses all of those concerns, and it will be interesting to see if it picks up any kind of steam. Formalising the existing use of Eclipse-style code templates with a more powerful system should have loads of promise.