Michael Soegtrop (Sep 04 2020 at 10:19): Michael Soegtrop (Sep 04 2020 at 10:19):I wonder if it is possible to write an inverse of M.fapp, that is a function with signature
Definition fMAMB_fMAB {A B : Type} (f : M A -> M B) : M (A -> B)
Can you give some context? Why do you want this function?
Michael Soegtrop (Sep 04 2020 at 11:53):I don't really need it - it was more curiosity. I don't think it is technically possible to write it using M.bind but I don't see a logical reason why it shouldn't be allowed. Let's say it is about understanding what M really means.
Or asked in another way: is M(A->B) stronger than M A -> M B. If so, is their an intuitive explanation for it?
The idea for having this function came from a few cases where I found it a bit hard to decide if I should type something <whatever> -> M A -> M B or <whatever> -> M (A->B). Having a conversion function in both directions would make such decision easier. I tend more towards the first but it is interesting that I can convert the second to the first but not vice versa, which would be a good reason to use the second in case it is possible.
Btw.: I am still mostly experimenting in the M.t domain since for most premises I know the type, but I guess I will come soon to ttac.
Paolo Giarrusso (Sep 04 2020 at 12:09):For arbitrary monads, there's a very good reason for not having this function: with M A -> M B, the "side effects" of the result can depend "dynamically" on the whole M A.
Paolo Giarrusso (Sep 04 2020 at 12:09):With M (A -> B), the side effects are fixed.
Paolo Giarrusso (Sep 04 2020 at 12:11):(and for related reasons, metaprograms on M A can do more if all the computations have type M (A -> B) — especially if the whole computation only uses the Applicative API on M. Simon Marlow’s talk on Haxl hinges on this point.)
Paolo Giarrusso (Sep 04 2020 at 12:12):if M itself is opaque, then functions of type M A -> M B can only inspect the A, so they have power similar to A -> M B (maybe the same power?), but a similar distinction applies.
Janno (Sep 04 2020 at 12:25):if M itself is opaque, then functions of type M A -> M B can only inspect the A, so they have power similar to A -> M B (maybe the same power?), but a similar distinction applies.
It is a bit more interesting in Mtac2 since Mtac2 can inspect Mtac2 terms and in that way f : M A -> M B is indeed more powerful than f : A -> M B. However, I struggle to come up with any good use case for this outside of exotic stuff that wouldn't come up in normal tactic programming.
Janno (Sep 04 2020 at 12:28):@Michael Soegtrop you can define your function this way: Definition fMAM_fMAB {A B : Type} (f : M A -> M B) : M (A -> B) := \nu a : A, f (M.ret a) >>= M.abs_fun a.
Michael Soegtrop (Sep 04 2020 at 12:42):@Paolo Giarrusso : many thanks for the detailed explanation!
@Janno : quite intriguing - I need to study how this solution works! It solves my original problem of deciding which formulation to use but it pushed me quite a bit right / down the Dunning-Kruger curve. I hope I reach the bottom soon ...
Paolo Giarrusso (Sep 04 2020 at 12:46):And to be sure, is that function actually inverse than fapp? The type matches but I wonder about the semantics
Paolo Giarrusso (Sep 04 2020 at 12:46):(no need to explain what happens beyond "are they inverses")
Michael Soegtrop (Sep 04 2020 at 13:09):Paolo Giarrusso said:
And to be sure, is that function actually inverse than fapp? The type matches but I wonder about the semantics
You mean if a tactic wrapped in either combination of M.fapp and fMAMB_fMAB would have strictly the same behavior as the original tactic? Indeed an interesting question.
Janno (Sep 04 2020 at 13:12):No, sorry, I wanted to mention that. I don't think there is a proper inverse.
Janno (Sep 04 2020 at 13:15):Of course there is this beauty here:
Definition fMAM_fMAB' {A B : Type} (f : M A -> M B) : M (A -> B) :=
mmatch f return M (A -> B) with
| [? f] @fapp A B f =u> f
end.
Even more intriguing ... doesn't this mean it is a proper (left) inverse? In case it is not - can you explain in which respect it is not a proper inverse?
Janno (Sep 04 2020 at 13:24):Evaluating fMAM_fMAB' also evaluatesf instead of returning it.
Janno (Sep 04 2020 at 13:25):I suppose we could add another layer of M in the return type and change the branch into M.ret f but then the types are different.
Beta Ziliani (Sep 04 2020 at 15:58):Janno said:
Of course there is this beauty here: [...]
Mr. Simpsons, you are diabolical!
I always wanted to know what kind of beast we have here, form a mathematical perspective. My intuition says that, by being able to inspect meta-programs (as Janno does in this definition), we are likely to break any possible understanding of it.
Paolo Giarrusso (Sep 04 2020 at 16:54):There might be some relevant prior work in research on well-typed reflection...
Paolo Giarrusso (Sep 04 2020 at 16:55):... Is the self-introspection a form of monadic reflection a la Filinski?
Paolo Giarrusso (Sep 04 2020 at 16:56):I guess I'd have to read more on mtac2 before more brainstorming, but my paper-reading budget is probably exhausted for now
Michael Soegtrop (Sep 04 2020 at 17:11):I have a question on the nu function. The tutorial says:
The effect of computing [nu n None (fun x=>b)], where [b : T B], is the result of
executing [b], replacing any occurrence of [x] with a fresh _parameter_ [a] named after [n]
I am struggling to understand what fresh parameter is technically. An evar?
Beta Ziliani (Sep 04 2020 at 17:12):no, a variable in the context (aka a hypothesis)
Beta Ziliani (Sep 04 2020 at 17:14):Paolo Giarrusso said:
... Is the self-introspection a form of monadic reflection a la Filinski?
I think it's more powerful than that, but I must check the details
Michael Soegtrop (Sep 04 2020 at 17:36):no, a variable in the context (aka a hypothesis)
Hmm, I don't understand how one can introduce a hypothesis which hasn't been there before. Is there a sequence of ltac commands which has a similar effect as nu and abs_fun?
Janno (Sep 04 2020 at 18:57):Is there a sequence of ltac commands which has a similar effect as nu and abs_fun?
No, there is nothing like that in Ltac1 and that's one of the biggest drawbacks of Ltac1. There might be workarounds for any specific instance where you would need this but nothing general that I am aware of. Ltac2 has the in_context primitive to provide nu + abs_fun in one but the construction is quite awkard.
Hmm, I don't understand how one can introduce a hypothesis which hasn't been there before.
The trick is to not let it escape the scope of nus continuation: the value nu returns cannot contain the new hypothesis. Play around with it, try to produce False out of thin air. You'll quickly get an intuition for why it's sound.
Beta Ziliani (Sep 05 2020 at 16:01):and please add your findings in the tutorial :-)
Michael Soegtrop (Sep 05 2020 at 17:20):@Janno : thanks for the explanation! I did play with it and think I have a good overview over what it does at a user perceivable level when combined with abs_fun. What I don't understand well is what internal term structure \nu a : False, M.ret a has - I guess it is just the application of the opaque function nu which is handled in the intended way by mrun. I guess it is not that important to be able to use it.
I agree that it is a very useful feature.
Last updated: Feb 06 2023 at 06:29 UTC