Hi all! Let's say i would like to write a monad transformer, but it will only be well defined for strictly positive monads. Eg the free-monad-over-a-functor transformer, `FreeT F M X := mu A. M (X + F A)`

(this is not the one i want to write, but it's a bit similar). For functors i'm ok with encoding them as containers/polynomial functor (operations and arities), but for monads it seems a bit painful. Going the full route of algebraic monad presentations (eg free monads over a polynomial functor + equations) is definitely out of the question (too many lines of code just to write an ugly version of the simple state monad). What is really upsetting is that for any particular instance of M that would be of interest to me (state, families, ..) and which coq would see as indeed strictly positive, then the code would be both quite direct and still mostly not dependent on peculiarities of M.

So: would there be by any chance an ugly hack one can pull to delay the guardedness/strict-positivity check until some variables are instanciated? Or does anyone see another way forward in this kind of case? Perhaps some syntax generating non-ugly decoded strictly-positive monads? @Kenji Maillard perhaps, would you say your syntax for monads from your PhD could be pratically useful here?

If you're happy with that, you could just plainly disable the guardedness/strict positivity check, and explain in a comment why this is not a problem

`Unset Strict Posititivity. Unset Guard Checking.`

For monads living in an impredicative sort, there is the well-known Mendler encoding that turns any functor into a syntactically strictly positive one that is equivalent assuming the input was already semantically strictly positive. But I guess you're talking about monads living in Type here.

@Yannick Forster Yes indeed i could do this in last resort, but i would be on my own to check that i didn't do bad stuff.. Also it would be nice to at least check that the parameter monad is strictly positive upon instanciation.

@Pierre-Marie Pédrot Yes i would be more interested in monads in Type. I guess i could try this anyway.. Writing eg:

`FreeT M F X := mu A. (Y : Set) * M Y * (Y -> F (X + A))`

..

You could define the inductive with strict positivity checking turned off, and then use MetaCoq (or another mega programming language) to turn the instantiation into a new inductive that can be given to Coq's positivity checker

Not a trivial task, but an interesting meta program I think

So this meta-program would take the whole parametrized module, a parameter, and then syntactically substitute to get the output module, right?

I don't think what I investigated during my phd could help here, it is ultimately limited by the expressiveness of the metatheory into which the monad definition language is written and decodes to. As you said, I think currently the proper generic approach to this question is to use containers/polynomial functors tracking the strict positivity witnesses for all your functors/monads (but it will most probably be painful, yes).

I would imagine something looking like this

```
#[bypass_check(positivity)]
Inductive Exp (F : Type -> Type) :=
| In : F (Exp F) -> Exp F.
Definition Nat X := (unit + X)%type.
MetaCoq Run Create Exp Nat as N.
Print N.
(* Inductive N : Type := In_N : Nat N -> N. *)
```

Of course, the command `MetaCoq Run Create Exp`

is not (yet) implemented :)

@Kenji Maillard Ok, indeed that's what i expected :/ In any case i learnt a lot of stuff reading it!

Update: the co-yoneda trick seems to be working miracles once again. @Pierre-Marie Pédrot do you remember what's the problem exactly when working in type?

Yannick Forster said:

Of course, the command

`MetaCoq Run Create Exp`

is not (yet) implemented :)

Ok, i will see how far the mendler encoding takes me and i will keep this tactic solution in mind. Anyway thanks a lot to everybody for these relevant suggestions.

Relevant reference: https://people.csail.mit.edu/bendy/MTC/MTC.pdf

Indirectly relevant reference, because it explains a bit why I'm advocating for ad hoc solutions with meta-programming: https://dl.acm.org/doi/abs/10.1145/3372885.3373817

Using the mendler encoding you obtain something too large, it's typically living in the universe succesor to what you expect (in particular it won't be an endofunctor and you won't be able to iterate it, so it's a bit annoying for the standard monad approach; I don't know whether a relative monad approach would work though)

Ah right, i forgot this size issue! Well, using the kleisli triple approach to monads one treats these monads relative to universe lifting quite seamlessly since the monad is never actually applied to itself.. I will see if i get stuck, but i'm more confident hacking with levels than with meta prog!

Last updated: Jun 23 2024 at 05:02 UTC