4 ms·

>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 e

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

ImprobableTruth 6y ago
>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.
- ivanbakel 6y ago
  >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.

ImprobableTruth 6y ago

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

ivanbakel 6y ago
>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.