feat(PFunctor): redefine PFunctor.FreeM in terms of PFunctor.W - #731
feat(PFunctor): redefine PFunctor.FreeM in terms of PFunctor.W#731dtumad wants to merge 6 commits into
PFunctor.FreeM in terms of PFunctor.W#731Conversation
| deriving Inhabited | ||
| /-- The free monad on a polynomial functor: the W-type of the polynomial functor obtained by\ | ||
| adjoining a constant shape for each pure value to `P`. -/ | ||
| def FreeM (P : PFunctor.{uA, uB}) (α : Type v) : Type (max uA uB v) := |
There was a problem hiding this comment.
Mathlib has increasingly come to the conclusion that newer lean versions are making it a bad idea to ever define a type with a def; either you should embrace the instances on the underyling type and use an abbrev, or make a one field structure with conversion constructors and projectors (toW and ofW).
There was a problem hiding this comment.
Done, that makes sense to me especially with the module system now. I also used AI in trying to identify standard API surface for similar definitions (injectivity, equivalence, etc.) but let me know if there's anything else that seems obvious.
I did also check that this doesn't break PolyFun definitions really, and I think we are probably the main consumer still.
|
|
||
| /-- The equivalence between the free monad and its underlying W-type, given by `FreeM.toW` | ||
| and `FreeM.ofW`. Both round-trips hold definitionally. -/ | ||
| def equivW : P.FreeM α ≃ PFunctor.W (P.add (.const α)) where |
There was a problem hiding this comment.
With the casting functions in place, my question now becomes: is there any advantage to actually changing the definition of FreeM vs just building this equivalence from the old definition?
There was a problem hiding this comment.
I guess I'd still think it is nice for the inverse laws of the equivalence to be definitional rfl rather than just propositional by induction, so that if we have say motive : P.FreeM A -> Sort u then we can use something of type motive (ofW (toW x)) as a motive x without needing a ▸ call.
I don't think this really escalates to Heq annoyance more generally, but it does seem maybe nice for that narrower situation? Not sure if that's enough to justify the change now.
| /-- The unit polynomial functor, defined as `A = PUnit` and `B _ = PEmpty`, is the identity with | ||
| respect to product (up to equivalence) -/ | ||
| @[reducible] protected def one : PFunctor := monomial PUnit PEmpty | ||
|
|
||
| instance instOnePFunctor : One PFunctor where one := PFunctor.one |
There was a problem hiding this comment.
I'd probably argue for inlining these, to avoid needing two spellings for the same thing:
| /-- The unit polynomial functor, defined as `A = PUnit` and `B _ = PEmpty`, is the identity with | |
| respect to product (up to equivalence) -/ | |
| @[reducible] protected def one : PFunctor := monomial PUnit PEmpty | |
| instance instOnePFunctor : One PFunctor where one := PFunctor.one | |
| /-- The unit polynomial functor is defined as `A = PUnit` and `B _ = PEmpty`, and is the identity with | |
| respect to product (up to equivalence) -/ | |
| instance : One PFunctor where one := monomial PUnit PEmpty |
There was a problem hiding this comment.
This is usually my feeling but I see sometimes monads for example defining a manual pure operation seperate from the instance so not sure on the usual conventions (I guess maybe for pure it is because the generic bind can be more universe generic than >>=).
| /-- The sum of two polynomial functors `P` and `Q`, written as `P + Q`, | ||
| defined as the sum of the head types and the sum case analysis for the child types. -/ | ||
| def add (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : | ||
| PFunctor.{max uA₁ uA₂, uB} := ⟨P.A ⊕ Q.A, Sum.elim P.B Q.B⟩ | ||
|
|
||
| instance instHAddPFunctor : | ||
| HAdd PFunctor.{uA₁, uB} PFunctor.{uA₂, uB} PFunctor.{max uA₁ uA₂, uB} where | ||
| hAdd := add |
There was a problem hiding this comment.
Similarly, do we need both here?
There was a problem hiding this comment.
I think so, or at least it seems useful with universe level changes because + notation seems to unify earlier (see tests in #803).
| @[simp] lemma add_B_inl (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (a : P.A) : | ||
| (add P Q).B (.inl a) = P.B a := rfl |
There was a problem hiding this comment.
This is ill-typed, because (add P Q).B is not a function from Sum _ _ but from (add P Q).A which isn't reducible
There was a problem hiding this comment.
Can I suggest you first make a PR that just adds this file, without the link to FreeM yet?
2 participants
Currently
PFunctor.FreeM P AandPFunctor.W (P.add (.const A))are equivalent but not definitionally equal, so proofs about one can't be translated over to the other automatically, they need to factor through aFreeM.toWandFreeM.ofWdefinition.This PR redefines
PFunctor.FreeMso that they are the same by construction. Case analysis lemmas are tagged with@[cases_eliminator]and@[induction_eliminator]so those tactics don't break (although manual pattern matching does). It also adds definitions ofPFunctor.monomialandPFunctor.addthat are used in the definition, and a short test file checking thatcasesandinductiondon't break.Definitions in
Basic.leanmostly come from downstream PolyFun library.