7 ms·

Towards Tactic Metaprogramming in Haskell

219 points by headalgorithm 6y ago

dllthomas 6y ago
> In actuality there are four different, valid programs that can be produced by the above set of tactics: [...] Nitpick, but only two of those are valid programs. Two of them use `a` without binding it.
- Benjmhart 6y ago
  Nitpick. But unused bindings is a warning, it doesn't create an invalid program
  - dllthomas 6y ago
    These are unbound usings.
    - yorwba 6y ago
      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.
      - Twisol 6y ago
        The article was edited in the interim. The error the ancestor posts describes did exist before (I saw it, too), but no longer.
      - dllthomas 6y ago
        As noted by Twisol, those holes previously contained `(fab a)`. I'd delete my comment now that it's addressed, but 1) it's too late, and 2) I'm too happy about "unbound usings".
- deleted 6y ago
  [deleted]
behnamoh 6y ago
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.
- creata 6y ago
  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.
  - momentoftop 6y ago
    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). There's nothing buzzwordy about this. [1] https://ui.adsabs.harvard.edu/abs/1984RSPTA.312..411M/abstract https://ui.adsabs.harvard.edu/abs/1984RSPTA.312..411M/abstra...
    - ImprobableTruth 6y ago
      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.
      - momentoftop 6y ago
ivanbakel 6y ago
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.
- ImprobableTruth 6y ago
  >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.
  - ivanbakel 6y ago
    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.
    - ImprobableTruth 6y ago
      >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.
mlang23 6y ago
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.
ImprobableTruth 6y ago
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?
- ivanbakel 6y ago
  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.
  - ImprobableTruth 6y ago
    >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".
tus88 6y ago
Crazy he serialized his thinking into a series of bytes referred to as a blog post.
- loa_in_ 6y ago
  He could just leave us a list of indexes into the English dictionary instead
xupybd 6y ago
Wow that guys writing style is very addictive. Just went on to read half his blog. I'd love to figure out how to write like that.
- zingplex 6y ago
  Sandy has some books you may want to check out. https://leanpub.com/u/sandy-maguire https://leanpub.com/u/sandy-maguire
  - whateveracct 6y ago
    The recently-released Algebra Driven Design is really fun.
    - iso8859-1 6y ago
      There is a reading group on Zulip: https://funprog.zulipchat.com/#narrow/stream/258464-Algebra-Driven.20Design https://funprog.zulipchat.com/#narrow/stream/258464-Algebra-...
    - dhab 6y ago
      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.
      - lgas 6y ago
        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.
voidhorse 6y ago
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.
- yorwba 6y ago
  > 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).
  - voidhorse 6y ago
    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.
imtringued 6y ago
>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.
- HoolaBoola 6y ago
  > Show me your semantic muscles and I'll change my mind. Wasn't the post basically doing just that?
fouric 6y ago
How is this anything but a renamed and unnecessarily-difficult-to-understand structure editor?

219 points by headalgorithm 6y ago

> In actuality there are four different, valid programs that can be produced by the above set of tactics: [...] Nitpick, but only two of those are valid programs. Two of them use `a` without binding it.

Benjmhart 6y ago
Nitpick. But unused bindings is a warning, it doesn't create an invalid program
- dllthomas 6y ago
  These are unbound usings.
  - yorwba 6y ago
    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.
    - Twisol 6y ago
      The article was edited in the interim. The error the ancestor posts describes did exist before (I saw it, too), but no longer.
    - dllthomas 6y ago
      As noted by Twisol, those holes previously contained `(fab a)`. I'd delete my comment now that it's addressed, but 1) it's too late, and 2) I'm too happy about "unbound usings".
deleted 6y ago
[deleted]

behnamoh 6y ago

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.

creata 6y ago
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.
- momentoftop 6y ago
  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). There's nothing buzzwordy about this. [1] https://ui.adsabs.harvard.edu/abs/1984RSPTA.312..411M/abstract https://ui.adsabs.harvard.edu/abs/1984RSPTA.312..411M/abstra...
  - ImprobableTruth 6y ago
    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.
    - momentoftop 6y ago

ivanbakel 6y ago

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.

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

mlang23 6y ago

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.

ImprobableTruth 6y ago

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?

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

tus88 6y ago

Crazy he serialized his thinking into a series of bytes referred to as a blog post.

loa_in_ 6y ago
He could just leave us a list of indexes into the English dictionary instead

xupybd 6y ago

Wow that guys writing style is very addictive. Just went on to read half his blog. I'd love to figure out how to write like that.

zingplex 6y ago
Sandy has some books you may want to check out. https://leanpub.com/u/sandy-maguire https://leanpub.com/u/sandy-maguire
- whateveracct 6y ago
  The recently-released Algebra Driven Design is really fun.
  - iso8859-1 6y ago
    There is a reading group on Zulip: https://funprog.zulipchat.com/#narrow/stream/258464-Algebra-Driven.20Design https://funprog.zulipchat.com/#narrow/stream/258464-Algebra-...
  - dhab 6y ago
    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.
    - lgas 6y ago
      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.

voidhorse 6y ago

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.

yorwba 6y ago
> 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).
- voidhorse 6y ago
  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.

imtringued 6y ago

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

HoolaBoola 6y ago
> Show me your semantic muscles and I'll change my mind. Wasn't the post basically doing just that?

fouric 6y ago

How is this anything but a renamed and unnecessarily-difficult-to-understand structure editor?