From ad48d8eac70dc4367260570ec4a62c6f9177a705 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 4 Dec 2024 15:45:23 +0000 Subject: [PATCH] refactor: remove `IsPolynomial` class (#55) I added the IsPolynomial typeclass as an experiment to see if we could use typeclass synthesis to keep track of QPFs whose quotient is trivial (in the sense that the QPF is isomorphic to the underlying polynomial functor). This hasn't really worked out, and as it stands the definition of IsPolynomial is broken: it takes in an [MvFunctor _] instance argument, even though it already extends MvQPF _, which was refactored to extend MvFunctor _, meaning we now have multiple instances of MvFunctor floating around. We could fix this fairly easily, but I think long-term it will be much easier to just write meta-code that optimistically keeps track of which QPFs are just PFunctors, rather than to use typeclass synthesis to recover this information after the fact. Thus, we should remove IsPolynomial alltogether --- Qpf/Macro/Comp.lean | 31 +++-- Qpf/Macro/Data.lean | 31 +---- .../Multivariate/Constructions/Prod.lean | 22 ++-- .../Multivariate/Constructions/Sum.lean | 8 +- Qpf/Qpf.lean | 2 - Qpf/Qpf/Multivariate/Basic.lean | 84 +------------ Qpf/Qpf/Multivariate/Constructions/Comp.lean | 85 ------------- .../Multivariate/Constructions/DeepThunk.lean | 4 +- Qpf/Qpf/Multivariate/Scratch.lean | 117 ++++++++++++++++++ Test/DeadWrap.lean | 2 +- 10 files changed, 155 insertions(+), 231 deletions(-) delete mode 100644 Qpf/Qpf/Multivariate/Constructions/Comp.lean create mode 100644 Qpf/Qpf/Multivariate/Scratch.lean diff --git a/Qpf/Macro/Comp.lean b/Qpf/Macro/Comp.lean index acf74d2..517befa 100644 --- a/Qpf/Macro/Comp.lean +++ b/Qpf/Macro/Comp.lean @@ -23,6 +23,7 @@ import Mathlib.Data.QPF.Multivariate.Constructions.Prj import Mathlib.Data.Vector.Basic import Qpf.Qpf +import Qpf.Qpf.Multivariate.Basic import Qpf.Macro.Common import Qq @@ -49,7 +50,7 @@ def synthMvFunctor {n : Nat} (F : Q(TypeFun.{u,u} $n)) : MetaM Q(MvFunctor $F) : q(MvFunctor $F) synthInstanceQ inst_type -def synthQPF {n : Nat} (F : Q(TypeFun.{u,u} $n)) (_ : Q(MvFunctor $F)) : MetaM Q(MvQPF $F) := do +def synthQPF {n : Nat} (F : Q(TypeFun.{u,u} $n)) : MetaM Q(MvQPF $F) := do let inst_type : Q(Type (u+1)) := q(MvQPF $F) synthInstanceQ inst_type @@ -87,10 +88,9 @@ where try -- Only try to infer QPF if `F` contains no live variables if !F.hasAnyFVar isLiveVar then - let F : Q(TypeFun.{u,u} $depth) - := q(TypeFun.ofCurried $F) - let functor ← synthMvFunctor F - let _ ← synthQPF F functor + let F : Q(TypeFun.{u,u} $depth) := + q(TypeFun.ofCurried $F) + let _ ← synthQPF F return ⟨depth, F, args⟩ throwError "Smallest function subexpression still contains live variables:\n {F}\ntry marking more variables as dead" catch e => @@ -106,8 +106,7 @@ where trace[QPF] "F := {F}\nargs := {args.toList}\ndepth := {depth}" let F : Q(TypeFun.{u,u} $depth) := q(TypeFun.ofCurried $F) - let functor ← synthMvFunctor F - let _ ← synthQPF F functor + let _ ← synthQPF F return ⟨depth, F, args⟩ @@ -213,7 +212,6 @@ partial def handleApp (vars : Vector FVarId arity) (target : Q(Type u)) : TermEl else let G ← args.mmap (elabQpf vars · none false) - let Ffunctor ← synthInstanceQ q(MvFunctor $F) let Fqpf ← synthInstanceQ q(@MvQPF _ $F) let G : Vec _ numArgs := fun i => G.get i.inv @@ -313,14 +311,17 @@ def elabQpfCompositionBody (view: QpfCompositionBodyView) : res.F.check res.qpf.check - withOptions (fun opt => opt.insert `pp.explicit true) <| do + let (F, qpf) ← withOptions (fun opt => opt.insert `pp.explicit true) <| do let F ← delab res.F let qpf ← delab res.qpf + pure (F, qpf) - withQPFTraceNode "results …" <| do - trace[QPF] "Functor := {F}" - trace[QPF] "MvQPF instance := {qpf}" - return ⟨F, qpf⟩ + withQPFTraceNode "results …" <| do + trace[QPF] "Functor (expr) := {res.F}" + trace[QPF] "Functor (stx) := {F}" + trace[QPF] "MvQPF (expr) := {res.qpf}" + trace[QPF] "MvQPF (stx) := {qpf}" + return ⟨F, qpf⟩ structure QpfCompositionView where @@ -385,10 +386,6 @@ def elabQpfComposition (view: QpfCompositionView) : CommandElabM Unit := do let F_applied ← `($F $deadBinderNamedArgs:namedArgument*) let cmd ← `( - $modifiers:declModifiers - instance : MvFunctor (TypeFun.ofCurried $F_applied) := - MvQPF.instMvFunctor_ofCurried_curried - $modifiers:declModifiers instance $deadBindersNoHoles:bracketedBinder* : MvQPF (TypeFun.ofCurried $F_applied) := MvQPF.instQPF_ofCurried_curried diff --git a/Qpf/Macro/Data.lean b/Qpf/Macro/Data.lean index a396601..02cc1c8 100644 --- a/Qpf/Macro/Data.lean +++ b/Qpf/Macro/Data.lean @@ -304,8 +304,8 @@ def mkQpf (shapeView : InductiveView) (ctorArgs : Array CtorArgs) (headT P : Ide map f x := ($eqv).invFun <| ($P).map f <| ($eqv).toFun <| x ) elabCommandAndTrace (header := "defining {q}") <|← `( - instance $q:ident : MvQPF.IsPolynomial (@TypeFun.ofCurried $(quote arity) $shape) := - .ofEquiv $P $eqv + instance $q:ident : MvQPF (@TypeFun.ofCurried $(quote arity) $shape) := + .ofEquiv (fun _ => $eqv) ) /-! ## mkShape -/ @@ -382,33 +382,6 @@ def mkShape (view : DataView) : TermElabM MkShapeResult := do mkQpf view ctorArgs headTId PId r.expr.size ⟩ -open Elab.Term Parser.Term in -/-- - Checks whether the given term is a polynomial functor, i.e., whether there is an instance of - `IsPolynomial F`, and return that instance (if it exists). --/ -def isPolynomial (view : DataView) (F: Term) : CommandElabM (Option Term) := - withQPFTraceNode "isPolynomial" (tag := "isPolynomial") <| - runTermElabM fun _ => do - elabBinders view.deadBinders fun _deadVars => do - let inst_func ← `(MvFunctor $F:term) - let inst_func ← elabTerm inst_func none - - trace[QPF] "F = {F}" - let inst_type ← `(MvQPF.IsPolynomial $F:term) - trace[QPF] "inst_type_stx: {inst_type}" - let inst_type ← elabTerm inst_type none - trace[QPF] "inst_type: {inst_type}" - - try - let _ ← synthInstance inst_func - let inst ← synthInstance inst_type - return some <|<- delab inst - catch e => - trace[QPF] "Failed to synthesize `IsPolynomial` instance.\ - \n\n{e.toMessageData}" - return none - /-- Take either the fixpoint or cofixpoint of `base` to produce an `Internal` uncurried QPF, and define the desired type as the curried version of `Internal` diff --git a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean index 0c36363..91ee803 100644 --- a/Qpf/PFunctor/Multivariate/Constructions/Prod.lean +++ b/Qpf/PFunctor/Multivariate/Constructions/Prod.lean @@ -6,31 +6,26 @@ import Mathlib.Data.QPF.Multivariate.Basic import Mathlib.Tactic.FinCases import Qpf.Util -import Qpf.Qpf.Multivariate.Basic namespace MvQPF namespace Prod open PFin2 (fz fs) -def P : MvPFunctor.{u} 2 := +def P : MvPFunctor.{u} 2 := .mk PUnit fun _ _ => PFin2 1 abbrev QpfProd' := P.Obj abbrev QpfProd := TypeFun.curried QpfProd' -/-- - An uncurried version of the root `Prod` --/ -abbrev Prod' : TypeFun 2 - := @TypeFun.ofCurried 2 Prod +/-- An uncurried version of the root `Prod` -/ +def Prod' : TypeFun 2 := + @TypeFun.ofCurried 2 Prod -/-- - Constructor for `QpfProd'` --/ -def mk (a : Γ 1) (b : Γ 0) : QpfProd'.{u} Γ := +/-- Constructor for `QpfProd'` -/ +def mk (a : Γ 1) (b : Γ 0) : QpfProd'.{u} Γ := ⟨ ⟨⟩, fun @@ -56,8 +51,9 @@ def equiv {Γ} : Prod' Γ ≃ QpfProd' Γ := { instance : MvFunctor Prod' where map f x := equiv.invFun <| P.map f <| equiv.toFun <| x -instance : MvQPF.IsPolynomial Prod' := .ofEquiv _ equiv - +instance : MvQPF Prod' := .ofEquiv (fun _ => equiv) +instance : MvQPF (@TypeFun.ofCurried 2 Prod) := + inferInstanceAs (MvQPF Prod') end Prod diff --git a/Qpf/PFunctor/Multivariate/Constructions/Sum.lean b/Qpf/PFunctor/Multivariate/Constructions/Sum.lean index e62f1bd..d51b988 100644 --- a/Qpf/PFunctor/Multivariate/Constructions/Sum.lean +++ b/Qpf/PFunctor/Multivariate/Constructions/Sum.lean @@ -6,7 +6,6 @@ import Mathlib.Data.QPF.Multivariate.Basic import Mathlib.Tactic.FinCases import Qpf.Util -import Qpf.Qpf.Multivariate.Basic namespace MvQPF namespace Sum @@ -38,7 +37,7 @@ def inr {Γ : TypeVec 2} (b : Γ 0) : QpfSum' Γ ⟩ -abbrev Sum' := @TypeFun.ofCurried 2 Sum +def Sum' := @TypeFun.ofCurried 2 Sum def box {Γ : TypeVec 2} : Sum' Γ → QpfSum' Γ | .inl a => inl a @@ -70,8 +69,9 @@ def equiv {Γ} : Sum' Γ ≃ QpfSum' Γ := instance : MvFunctor Sum' where map f x := equiv.invFun <| SumPFunctor.map f <| equiv.toFun <| x -instance : MvQPF.IsPolynomial Sum' := - .ofEquiv _ equiv +instance : MvQPF Sum' := .ofEquiv @equiv +instance : MvQPF (@TypeFun.ofCurried 2 Sum) := + inferInstanceAs (MvQPF Sum') end Sum diff --git a/Qpf/Qpf.lean b/Qpf/Qpf.lean index 2127c89..c5fb806 100644 --- a/Qpf/Qpf.lean +++ b/Qpf/Qpf.lean @@ -1,6 +1,4 @@ -import Qpf.Qpf.Multivariate.Basic - import Qpf.PFunctor.Multivariate.Basic import Qpf.PFunctor.Multivariate.Constructions.Arrow import Qpf.PFunctor.Multivariate.Constructions.Prod diff --git a/Qpf/Qpf/Multivariate/Basic.lean b/Qpf/Qpf/Multivariate/Basic.lean index f235665..b28c324 100644 --- a/Qpf/Qpf/Multivariate/Basic.lean +++ b/Qpf/Qpf/Multivariate/Basic.lean @@ -2,86 +2,14 @@ import Mathlib.Data.QPF.Multivariate.Basic import Qpf.Util.TypeFun namespace MvQPF - /-- - A QPF is polynomial, if it is equivalent to the underlying `MvPFunctor`. - `repr_abs` is the last property needed to show that `abs` is an isomorphism, with `repr` - its inverse - -/ - class IsPolynomial {n} (F : TypeVec n → Type _) extends MvQPF F where - repr_abs : ∀ {α} (x : P.Obj α), repr (abs x) = x - - - namespace IsPolynomial - variable {n : ℕ} {F : TypeVec n → Type _} - - /-- - Show that the desired equivalence follows from `IsPolynomial` - -/ - def equiv [MvFunctor F] [p : IsPolynomial F] : - ∀ α, F α ≃ p.P.Obj α - := fun _ => { - toFun := p.repr, - invFun := p.abs, - left_inv := p.abs_repr, - right_inv := p.repr_abs, - } - - def ofEquiv (P : MvPFunctor n) (eqv : ∀ {α}, F α ≃ P.Obj α) [functor : MvFunctor F] (map_eq : ∀ (α β : TypeVec n) (f : TypeVec.Arrow α β) (x : F α), functor.map f x = (eqv.invFun <| P.map f <| eqv.toFun <| x) := by intros; rfl) : IsPolynomial F where - P := P - abs := eqv.invFun - repr := eqv.toFun - abs_repr := eqv.left_inv - abs_map := by intros; - simp only [Equiv.invFun_as_coe, map_eq, Equiv.toFun_as_coe, - Equiv.apply_symm_apply, Equiv.symm_apply_apply, EmbeddingLike.apply_eq_iff_eq]; - rfl - repr_abs := eqv.right_inv - - end IsPolynomial - -end MvQPF - -namespace MvPFunctor - variable {n : Nat} (P : MvPFunctor n) - - /-- - Every polynomial functor is trivially a QPF - -/ - instance : MvQPF P.Obj := - { - P := P, - abs := id, - repr := id, - abs_repr := by intros; rfl, - abs_map := by intros; rfl, - } - - /-- - Every polynomial functor is a polynomial QPF - -/ - instance : MvQPF.IsPolynomial P.Obj := - { - repr_abs := by intros; rfl - } - -end MvPFunctor - - variable {n} {F : TypeFun n} -namespace MvQPF - instance instMvFunctor_ofCurried_curried [f : MvFunctor F] : - MvFunctor <| TypeFun.ofCurried <| F.curried := - TypeFun.ofCurried_curried_involution ▸ f - - instance instQPF_ofCurried_curried [MvFunctor F] [q : MvQPF F] : - MvQPF <| TypeFun.ofCurried <| F.curried := - TypeFun.ofCurried_curried_involution ▸ q +instance instMvFunctor_ofCurried_curried [f : MvFunctor F] : + MvFunctor <| TypeFun.ofCurried <| F.curried := + TypeFun.ofCurried_curried_involution ▸ f - instance instIsPolynomial_ofCurried_curried [functor : MvFunctor F] [p : IsPolynomial F] : - IsPolynomial <| TypeFun.ofCurried <| F.curried := by - apply cast ?_ p - congr - · rw [TypeFun.ofCurried_curried_involution] +instance instQPF_ofCurried_curried [q : MvQPF F] : + MvQPF <| TypeFun.ofCurried <| F.curried := + TypeFun.ofCurried_curried_involution ▸ q end MvQPF diff --git a/Qpf/Qpf/Multivariate/Constructions/Comp.lean b/Qpf/Qpf/Multivariate/Constructions/Comp.lean deleted file mode 100644 index 664b414..0000000 --- a/Qpf/Qpf/Multivariate/Constructions/Comp.lean +++ /dev/null @@ -1,85 +0,0 @@ -/- -Copyright (c) 2023 Alex Keizer. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Alex Keizer --/ - -import Mathlib.Data.QPF.Multivariate.Basic -import Mathlib.Data.QPF.Multivariate.Constructions.Comp -import Qpf.Util - -/-! - Show that the composition of polynomial QPFs is itself a polynomial QPF --/ - -universe u - -namespace MvQPF.Comp - -open MvPFunctor MvFunctor - -variable {n m : ℕ} - (F : TypeFun n) - (G : Vec (TypeFun m) n) - [p : IsPolynomial F] - [p' : ∀ i, IsPolynomial <| G i] - - - instance : IsPolynomial (Comp F G) where - repr_abs := by - intros α x; - rcases x with ⟨⟨a', f'⟩, f⟩ - simp only [Comp.get, Comp.mk, Function.comp_apply, repr, abs, ← p.abs_map, p.repr_abs] - simp only [(· <$$> ·), MvPFunctor.map, comp.mk, comp.get, TypeVec.comp] - congr 2 - { - funext i b - rw[(p' i).repr_abs] - } - { - apply HEq.funext - . simp only [IsPolynomial.repr_abs]; rfl - intro i - - have type_eq_α : B (comp (P F) fun i => P (G i)) - { fst := a', - snd := fun x a => - (repr (abs { fst := f' x a, snd := fun j b => f j { fst := x, snd := { fst := a, snd := b } } })).fst } - i = - B (P (Comp F G)) { fst := a', snd := f' } i := - by simp only [IsPolynomial.repr_abs]; rfl - - apply HEq.funext' - case type_eq_β => - intros; rfl - case type_eq_α => - exact type_eq_α - - rintro ⟨b, ⟨b', g'⟩⟩ - simp only [heq_eq_eq] - - have : repr (abs - ⟨ f' b b', - fun j b_1 => - f j ⟨b, ⟨b', b_1⟩⟩ - ⟩) - = ⟨ f' b b', - fun j b_1 => - f j ⟨b, ⟨b', b_1⟩⟩ - ⟩; - { - simp [IsPolynomial.repr_abs] - } - simp[type_eq_α, this] - /- - TODO: properly finish this proof - -/ - sorry - } - - - - - - -end MvQPF.Comp diff --git a/Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean b/Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean index ec3992a..2532d44 100644 --- a/Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean +++ b/Qpf/Qpf/Multivariate/Constructions/DeepThunk.lean @@ -62,8 +62,8 @@ instance : MvFunctor DTSum.Uncurried where map f := equiv.invFun ∘ Sum.SumPFunctor.map f ∘ equiv.toFun open DTSum in -instance : MvQPF.IsPolynomial DTSum.Uncurried := - .ofEquiv _ equiv +instance : MvQPF DTSum.Uncurried := + .ofEquiv (fun _ => equiv) namespace DeepThunk diff --git a/Qpf/Qpf/Multivariate/Scratch.lean b/Qpf/Qpf/Multivariate/Scratch.lean new file mode 100644 index 0000000..a84797d --- /dev/null +++ b/Qpf/Qpf/Multivariate/Scratch.lean @@ -0,0 +1,117 @@ +import Qpf +import Mathlib.Data.QPF.Multivariate.Constructions.Sigma + +#check MvPFunctor + +/-! +# Interaction Trees + +We define interaction trees, a coinductive data-structure used for giving +semantics of side-effecting, possibly non-terminating, programs + +[1] https://arxiv.org/abs/1906.00046 +[2] https://github.com/DeepSpec/InteractionTrees +-/ + +set_option trace.QPF true +-- set_option diagnostics true + +-- codata ITree (E : Type → Type) A where +-- | ret (r : A) +-- | tau (t : ITree E A) +-- | vis (_ : (Ans : Type) × ( E Ans) × ( Ans → ITree E A)) +-- -- vis : {Ans : Type} -> (e : E Ans) -> (k : Ans -> ITree E A) -> ITree E A + +section HeadChild + inductive ITree.HeadT : Type 1 + | ret + | tau + | vis (Ans : Type) + + def ITree.ChildT : ITree.HeadT -> TypeVec.{1} 2 + | .ret => ![PFin2.{1} 1, PFin2.{1} 0] -- One `A`, zero `ρ` + | .tau => ![PFin2.{1} 0, PFin2.{1} 1] -- Zero `A`, one `ρ` (remember, `ρ` intuitively means `ITree E A`) + | .vis Ans => ![PFin2.{1} 0, ULift.{1, 0} Ans] -- Zero `A`, and... `Ans` many `ρ`... -- ! where do we get Ans from? + + abbrev ITree.P : MvPFunctor.{1} 2 := ⟨ITree.HeadT, ITree.ChildT⟩ + abbrev ITree.F : TypeVec.{1} 2 -> Type 1 := ITree.P.Obj + + def ITree.box : F α → P.Obj α := sorry + def ITree.unbox : P.Obj α → F α := sorry + def ITree.box_unbox_id : (x : P.Obj α) -> box (unbox x) = x := sorry + def ITree.unbox_box_id : (x : F α) -> unbox (box x) = x := sorry + instance ITree.instMvQPF : MvQPF ITree.F := MvQPF.ofPolynomial P box unbox box_unbox_id unbox_box_id sorry + + def ITree_ugly := MvQPF.Cofix ITree.F -- you could do it this way, but it will be very unwieldy. Hence shape types. +end HeadChild + +set_option pp.universes true + +section ShapeBase + inductive ITree.Shape (E : Type -> Type) (A : Type 1) (ρ : Type 1) (ν : Type 1) : Type 1 + | ret (r : A) : ITree.Shape E A ρ ν + | tau (t : ρ) : ITree.Shape E A ρ ν + | vis (e : ν) : ITree.Shape .. + -- | vis : (Ans : Type) × E Ans × (Ans → ρ) -> ITree.Shape E A ρ + + -- qpf ITree.Base (E : Type -> Type) (A : Type) ρ := ITree.Shape E A ρ ((Ans : Type) × ULift.{1} (E Ans) × (Ans → ρ)) + -- ! If only we had this instance... life would be so easy + -- instance {E : Type -> Type} : MvQPF (TypeFun.ofCurried (n := 1) (ITree.Shape E A)) := sorry + -- def ITree' (E : Type -> Type) (A : Type 1) : TypeFun.{1} 0 := + -- MvQPF.Cofix (TypeFun.ofCurried <| ITree.Shape E A) + + /-- `qpf G (Ans : Type) (E : Type → Type) A ρ ν := E Ans × (Ans → ρ)`, but universe-polymorphic -/ + abbrev G.Uncurried (Ans : Type 0) (E : Type 0 → Type 0) : TypeFun.{1, 1} 2 := + MvQPF.Comp (n := 2) (m := 2) -- compose two 2-ary (A, ρ) functors `E Ans` and `Ans -> ρ` + (TypeFun.ofCurried Prod.{1, 1}) + -- (MvQPF.Prod.Prod') + ( + (Vec.append1 Vec.nil (MvQPF.Const 2 <| ULift (E Ans))).append1 + (MvQPF.Comp (n := 1) (m := 2) + (TypeFun.ofCurried (MvQPF.Arrow Ans)) + (Vec.append1 Vec.nil (MvQPF.Prj 1)) + ) + ) + + -- Ideally we'd do this directly, but the QPF meta code isn't there yet -- qpf G_vis (E : Type -> Type) A ρ ν := (Ans : Type) × (E Ans × (Ans -> ρ)) + abbrev G_vis.Uncurried (E : Type → Type) : TypeFun.{1,1} 2 := + MvQPF.Sigma.{1} fun (Ans : Type) => (G.Uncurried Ans E) + qpf G_ret (E : Type -> Type) A ρ := A + qpf G_tau (E : Type -> Type) A ρ := ρ + + set_option trace.Meta.synthInstance true + + #check MvQPF.Prod.instMvFunctorProd' + instance : MvQPF (TypeFun.ofCurried (n := 2) @Prod.{u}) := + sorry + + instance (i : PFin2 1) : MvQPF (Vec.append1 Vec.nil (MvQPF.Prj (n:=2) 1) i) := sorry + #synth ∀i : PFin2 1, MvQPF (Vec.append1 Vec.nil (MvQPF.Prj (n:=2) 1) i) + instance {Ans} {E : Type -> Type} : MvQPF.{1, 1} (G.Uncurried Ans E) := inferInstance + instance {Ans} {E : Type -> Type} : MvQPF.{1, 1} (G.Uncurried Ans E) := inferInstance + instance {E : Type -> Type} : MvQPF.{1, 1} (G_vis.Uncurried E) := inferInstance + + abbrev ITree.ConstructorFs (E : Type -> Type) : Fin2 3 -> TypeVec 2 -> Type 1 := + ![G_ret.Uncurried E, G_tau.Uncurried E, G_vis.Uncurried E] + + abbrev ITree.Base.Uncurried (E : Type -> Type) : TypeFun 2 := + MvQPF.Comp (TypeFun.ofCurried (n := 3) (ITree.Shape E)) (ITree.ConstructorFs E) + + -- def ITree.Base.Uncurried' (E : Type -> Type) : TypeFun 2 := fun v => ITree.Shape E (v 1) ((ITree.ConstructorFs E) 0 v) -- what am I even doing + abbrev ITree.Base (E : Type -> Type) (A ρ : Type 1) : Type 1 := + MvQPF.Comp (TypeFun.ofCurried (n := 3) (ITree.Shape E)) (ITree.ConstructorFs E) ![A, ρ] + + instance {E : Type -> Type} : MvQPF.{1, 1} (ITree.Base.Uncurried E) := inferInstance + + def ITree.Uncurried (E : Type -> Type) := + MvQPF.Cofix (ITree.Base.Uncurried E) +end ShapeBase + +instance {E : Type -> Type} : MvQPF (ITree.Base.Uncurried E) := sorry + +def ITree.Uncurried (E : Type -> Type) := MvQPF.Cofix (ITree.Base.Uncurried E) +def ITree (E : Type -> Type) (A : Type 1) : Type 1 := MvQPF.Cofix (ITree.Base.Uncurried E) ![A, A] -- ! why two + +#reduce (types := true) TypeVec.{1} 2 + +#check 1 diff --git a/Test/DeadWrap.lean b/Test/DeadWrap.lean index 4bf8524..7c0ce5d 100644 --- a/Test/DeadWrap.lean +++ b/Test/DeadWrap.lean @@ -18,6 +18,6 @@ data DeadWrap (α : Type) β /-- info: DeadWrap.Shape.qpf -/ #guard_msgs in - #synth MvQPF.IsPolynomial <| @TypeFun.ofCurried 3 DeadWrap.Shape + #synth MvQPF <| @TypeFun.ofCurried 3 DeadWrap.Shape end Test