Stream: MetaCoq

Topic: `tmFix`point combinator


view this post on Zulip Jason Gross (Nov 21 2022 at 18:46):

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

view this post on Zulip 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.

view this post on Zulip 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...)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Jason Gross (Nov 21 2022 at 21:10):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Jason Gross (Nov 21 2022 at 22:39):

whereas the definition of tmFix is

How is the definition of tmFix inconsistent?

view this post on Zulip Jason Gross (Nov 21 2022 at 22:41):

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

view this post on Zulip Jason Gross (Nov 21 2022 at 22:50):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Yannick Forster (Nov 21 2022 at 22:59):

and n = S n is inconsistent

view this post on Zulip Yannick Forster (Nov 21 2022 at 22:59):

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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Nov 21 2022 at 23:01):

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

view this post on Zulip Yannick Forster (Nov 21 2022 at 23:02):

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

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Yannick Forster (Nov 21 2022 at 23:09):

Because TM : Type -> Type

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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).?

view this post on Zulip 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?

view this post on Zulip Yannick Forster (Nov 21 2022 at 23:42):

I think in the end the counting is not even necessary

view this post on Zulip 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.

view this post on Zulip Yannick Forster (Nov 21 2022 at 23:43):

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

view this post on Zulip Yannick Forster (Nov 21 2022 at 23:44):

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

view this post on Zulip 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.

view this post on Zulip Jason Gross (Nov 22 2022 at 00:05):

I guess we should stick with the typeclass based one

view this post on Zulip 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

view this post on Zulip 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: Jan 30 2023 at 17:03 UTC