Stream: MetaCoq

Topic: `tmFix`point combinator

Jason Gross (Nov 21 2022 at 18:46):

Any thoughts on what to do with https://github.com/MetaCoq/metacoq/pull/784?

Théo Winterhalter (Nov 21 2022 at 19:35):

I don't know if I'd be happy turning off guard checking (even locally) in MetaCoq.

Jason Gross (Nov 21 2022 at 19:47):

What about adding it as another constructor to the template monad instead? (I'm not familiar with how the current template monad is hooked up, but I could try to write a PR for this.)

(Alternatively I could probably throw together a very hacky implementation in terms of tmInferInstance, but that seems worse than the other two alternatives...)

Pierre-Marie Pédrot (Nov 21 2022 at 20:16):

Adding a fixpoint like this returning an inductive type is inconsistent, not sure whether you care about that.

Yannick Forster (Nov 21 2022 at 21:01):

my take would be that everybody who wants to run a non-terminating Fixpoint should locally unset guard checking - not least for transparency reasons

Yannick Forster (Nov 21 2022 at 21:01):

Do you really need the combinator Jason, or do you just use it a couple of times?

Jason Gross (Nov 21 2022 at 21:10):

Oh, I guess having this as a constructor makes the inductive non-positive :-/ Grrr

Jason Gross (Nov 21 2022 at 21:11):

@Yannick Forster I need it for monad_trans in https://github.com/MetaCoq/metacoq/pull/776/files. I could fuel it instead, but that's sort of ugly. Do you see a better way?

Jason Gross (Nov 21 2022 at 22:31):

@Pierre-Marie Pédrot What do you mean? Here's an implementation that passes the guard checker (only for the core template monad; if I want one in the extractable template monad I need a version of tmUnquote for that (presumably routing through the native compiler, though I suspect that'll be painfully slow))

(** XXX FIXME THIS IS A HACK *)
Class HasFix := tmFix_ : forall {A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B)), A -> TemplateMonad B.
(* idk why this is needed... *)
#[local] Hint Extern 1 (Monad _) => refine TemplateMonad_Monad : typeclass_instances.
Definition tmFix {A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B)) : A -> TemplateMonad B
  := f
       (fun a
        => tmFix <- tmInferInstance None HasFix;;
           match tmFix with
           | my_Some tmFix => tmFix _ _ f a
           | my_None => tmFail "Internal Error: No tmFix instance"
           end).
#[global] Hint Extern 0 HasFix => refine @tmFix : typeclass_instances.

Yannick Forster (Nov 21 2022 at 22:36):

I would have expected that you can define monad_trans as Fixpoint with disabled guardedness checking. That's similar to right now, but I think it's not inconsistent, whereas the definition of tmFix is

Jason Gross (Nov 21 2022 at 22:38):

@Yannick Forster Note that I'm not wanting to run a fixpoint on the term level, but wanting an unbounded looping construct for the template monad itself. That is, I only want to have unbounded recursion inside MetaCoq Run / run_template_program. The use-case is that I want to recursively look up the body of an inductive in the environment, and there's no way to efficiently determine ahead of time how many nested calls this will require (recursive quoting of the environment is too slow for my use-case).

Jason Gross (Nov 21 2022 at 22:39):

whereas the definition of tmFix is

How is the definition of tmFix inconsistent?

Jason Gross (Nov 21 2022 at 22:41):

It allows me to inhabit TemplateMonad False, but I can already inhabit that with tmFail.

Jason Gross (Nov 21 2022 at 22:50):

I've pushed the alternative to https://github.com/MetaCoq/metacoq/pull/790

Yannick Forster (Nov 21 2022 at 22:56):

It's inconsistent for a version of TemplateMonad : Type -> Type I think - I'm not so sure about the Prop version

Yannick Forster (Nov 21 2022 at 22:57):

The reason is that

From MetaCoq.Template Require Import All Loader.

Local Unset Guard Checking.
Definition tmFix_body
           {A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B))
           (tmFix : unit -> A -> TemplateMonad B)
  := f (fun a => tmFix tt a).
Definition tmFix {A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B)) : A -> TemplateMonad B
  := (fix tmFix (dummy : unit) {struct dummy} : A -> @TemplateMonad B
      := tmFix_body f tmFix) tt.
Local Set Guard Checking.

Definition bla := tmFix (fun f (x : unit) => tmQuote (f tt)).

Goal bla tt = tmQuote (bla tt).
Proof.
  reflexivity.
Qed.

Yannick Forster (Nov 21 2022 at 22:58):

And now for an inductive type x = C x for C being a constructor of this type is a problem

Yannick Forster (Nov 21 2022 at 22:59):

For instance, if I would write a function recursing on an inductive element of TemplateMonad and counting how often a tmQuote constructor occurs stacked on the top, then this equation lets me prove n = S n for n being size (bla tt)

Yannick Forster (Nov 21 2022 at 22:59):

and n = S n is inconsistent

Yannick Forster (Nov 21 2022 at 22:59):

Actually I learned about such problems from PMP not too long ago

Yannick Forster (Nov 21 2022 at 23:00):

Whether this really applies for the monad in Prop I'm not sure, but it still looks strange to me

Paolo Giarrusso (Nov 21 2022 at 23:01):

It should apply for subsingleton Props like Acc, but I guess that's not TemplateMonad?

Yannick Forster (Nov 21 2022 at 23:02):

Yes, direct computation of the size will fail because TemplateMonad is a proposition

Paolo Giarrusso (Nov 21 2022 at 23:02):

And if the Prop isn't subsingleton, it seems the same reasoning should only prove proof irrelevance?

Yannick Forster (Nov 21 2022 at 23:08):

Okay, convinced, it won't be inconsistent for TemplateMonad. But the suggested tmFix will also apply to the extractable monad TM, and there it will be inconsistent (with a similar example but using tmBind instead of tmQuote)

Yannick Forster (Nov 21 2022 at 23:09):

Because TM : Type -> Type

Yannick Forster (Nov 21 2022 at 23:10):

Changing it to be a CoInductive might fix things once again, but given that there are easier ways out I'd say lets go with the easier ways

Jason Gross (Nov 21 2022 at 23:34):

@Yannick Forster Oh, that is interesting, thanks for the example! What about if instead we do

Definition tmFix_body
           {A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B))
           (tmFix : unit -> A -> TemplateMonad B)
  := f (fun a => tmBind (tmReturn tmFix) (fun tmFix => tmFix tt a)).

?

Now the loopy recursion is blocked by tmBind (tmReturn ...), and I think there shouldn't be any way to bypass it. There's no way to directly inspect tmFix for anything, and so you can't tell the difference between tmReturn tmFix and something like tmInferInstance, right?

Yannick Forster (Nov 21 2022 at 23:37):

My intuition the last time was that unsetting guard checking on inhabited return types is consistent. That was quickly debunked by PMP with an example. I at least can't come up with a problematic example for your suggested change, but I also don't have any intuition whether it's fine or not

Yannick Forster (Nov 21 2022 at 23:38):

I think the question boils down to is C (fun _ => x) = x consistent for Inductive T : Type := C (f : unit -> T).?

Jason Gross (Nov 21 2022 at 23:42):

Ah, and I guess it's not, because we can pull the same counting trick with match v with C f => S (f tt) end or something?

Yannick Forster (Nov 21 2022 at 23:42):

I think in the end the counting is not even necessary

Yannick Forster (Nov 21 2022 at 23:42):

Inductive T := C (f : unit -> T).

Goal forall x : T, C (fun _ => x) = x -> False.
Proof.
  induction x.
  intros E.
  inversion E.
  eapply (H tt).
  rewrite <- H1.
  f_equal. eauto.
Qed.

Yannick Forster (Nov 21 2022 at 23:43):

I used it earlier because dealing with the very dependent constructors of TM is annoying

Yannick Forster (Nov 21 2022 at 23:44):

So my intuition would be that we're still in danger zone with this fix

Jason Gross (Nov 22 2022 at 00:05):

Why would the unguarded monad_trans be any better, then? I think I could probably exhibit an infinite codepath or similar from it.

Jason Gross (Nov 22 2022 at 00:05):

I guess we should stick with the typeclass based one

Yannick Forster (Nov 22 2022 at 00:09):

If that's an option, I think it's a good option :) It's also not a problem to have inconsistent axioms around - after all MetaCoq comes with Axiom todo : forall A, A - but it's good to limit them and make them easy to identify

Yannick Forster (Nov 22 2022 at 00:10):

For monad_trans I don't have enough intuition to tell whether it's inconsistent or not - maybe it is

Last updated: Jun 01 2023 at 11:01 UTC