Error: «Introduced symbol cannot be removed.» Feature proposal job: primitive structure/record types to pack multiple arguments

[1337777]

1. Test problem:

constant symbol Set : TYPE;
injective symbol τ : Set → TYPE; builtin "T" ≔ τ;

symbol mys : TYPE;
symbol myop :  mys →  mys →   mys;

symbol testfun : Π (Func : Set) (Hom : τ Func → Set) (Comp : Π [F : τ Func]  , τ (Hom F)) ,
 mys;

// RULE ERROR: "Introduced symbol [$179144] cannot be removed."
rule (myop (@testfun $Func $Hom $Comp ) (@testfun $Func $Hom $Comp    ) )
    ↪  (@testfun $Func $Hom $Comp ) ;

2. Could anyone clarify what this error means? Temporary solution: this is solved by packing all the arguments of testfun into one value of a new inductive record/structure type.

3. Any future plans for an implementation of automatic/better support of structure/records with (primitive) projections in Lambdapi ?

4. Could the Lambdapi unif_rule command be used to simulate type classes or canonical structures, for (very) large library developments?

5. Here is the context: I have a Lambdapi implementation of Dosen's categorial logic/programming/proof-assistant with "abstract" automatic decidability of equality/convertibility, where "abstract" means that it is in reality a proof-assistant for proving categorial lemmas.

https://github.com/1337777/cartier/blob/master/cartierSolution13.lp

Now the next step is to link the "abstract" implementation to a "concrete" implementation of categorial datatype structures for concrete computations, everything still within Lambdapi.

6. And Lambdapi is currently the only framework, because of logical-dependent types and computational-rewrite rules, capable of merging both the "abstract" implementation for computationally-proving with the "concrete" implementation for computing, with categories... For example,

https://explore.jobs.ufl.edu/en-us/job/527710/systems-adminprogrammer-iv

in this AlgebraicJulia, for a "type-safe concrete" implementation, they have to hack a pseudo-dependent-type domain-specific-language embedded within Julia...

7. Proposal: Lambdapi could employ somebody (or me) this 1 month of August to engineer tooling support for typeclasses or canonical-structures in Lambdapi.. and thereafter to produce a "concrete" (applied) implementation of categories which is linked to the existing "abstract" (prover) implementation. And I repeat that Lambdapi is currently in a unique strategic position to unify both worlds with a limitless payoff, n.b. that some entities linked above are already investing $100,000 - $130,000 (in a limited approach) ...

Voilà, à vous!
Christopher

[fblanqui]

Hi @1337777 . Thanks for your report.
2. This is a bug in unification. I will commit a patch soon.
3. No such plan at the moment. Which kind of support would you like?
4. In theory, yes, but this has not been extensively tested yet. An alternative is to use #418 which adds type classes in Lambdapi using ELPI.