Stream: Coq users

Topic: the hopeless search for compositional strict positivity


view this post on Zulip Lapinot (Oct 27 2023 at 11:09):

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?

view this post on Zulip Yannick Forster (Oct 27 2023 at 11:17):

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

view this post on Zulip Yannick Forster (Oct 27 2023 at 11:17):

Unset Strict Posititivity. Unset Guard Checking.

view this post on Zulip Pierre-Marie Pédrot (Oct 27 2023 at 11:20):

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.

view this post on Zulip Lapinot (Oct 27 2023 at 12:19):

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

view this post on Zulip Yannick Forster (Oct 27 2023 at 12:21):

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

view this post on Zulip Yannick Forster (Oct 27 2023 at 12:21):

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

view this post on Zulip Lapinot (Oct 27 2023 at 12:23):

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

view this post on Zulip Kenji Maillard (Oct 27 2023 at 12:26):

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

view this post on Zulip Yannick Forster (Oct 27 2023 at 13:25):

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

view this post on Zulip Yannick Forster (Oct 27 2023 at 13:25):

Of course, the command MetaCoq Run Create Exp is not (yet) implemented :)

view this post on Zulip Lapinot (Oct 27 2023 at 13:26):

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

view this post on Zulip Lapinot (Oct 27 2023 at 13:28):

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.

view this post on Zulip Yannick Forster (Oct 27 2023 at 13:29):

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

view this post on Zulip Yannick Forster (Oct 27 2023 at 13:30):

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

view this post on Zulip Kenji Maillard (Oct 27 2023 at 13:31):

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)

view this post on Zulip Lapinot (Oct 27 2023 at 13:51):

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