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?

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.

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.

With M (A -> B), the side effects are fixed.

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

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.

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.

@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`

.

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

And to be sure, is that function actually inverse than fapp? The type matches but I wonder about the semantics

(no need to explain what happens beyond "are they inverses")

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.

No, sorry, I wanted to mention that. I don't think there is a proper inverse.

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?

Evaluating `fMAM_fMAB'`

also evaluates`f`

instead of returning it.

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.

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.

There might be some relevant prior work in research on well-typed reflection...

... Is the self-introspection a form of monadic reflection a la Filinski?

I guess I'd have to read more on mtac2 before more brainstorming, but my paper-reading budget is probably exhausted for now

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?

no, a variable in the context (aka a hypothesis)

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

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?

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 `nu`

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

and please add your findings in the tutorial :-)

@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