Login
You're viewing the discuss.systems public feed.
  • Amélia Liao 🍊😈amy@types.pl
    Oct 15, 2026, 12:57 PM

    @MartinEscardo what matters for typetopology: we've optimised lexing, parsing, handling of names (these primarily affect time spent in garbage collection), implemented a faster hashtable for serialisation, changed the semantics of -j to avoid a minor-but-quadratic overhead in worker startup (in addition to properly sharing project (= agda-lib file) state across workers), optimised syntactic equality, optimised metavariable pruning, removed a quadratic overhead from the types of metavariables, optimised the representation of and a bunch of code that deals with telescopes (≈ contexts), and made it so parameterised module applications only "pay" for the definitions they actually use¹

    ¹ in some libraries (1lab, agda-categories) this was a lot of the typechecker time, but typetopology only spends ~5s in the ApplySection profiling point so it shouldn't affect its timing too much.

    @de_Jong_Tom @totbwf

    💬 1🔄 1⭐ 1

Replies

  • 💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • 💬 1🔄 0⭐ 0
  • Amélia Liao 🍊😈amy@types.pl
    Oct 16, 2026, 5:11 PM

    @MartinEscardo yes. because of issues like !115 the termination checker is less willing to consider arguments whose type is only revealed to be (a function into) an inductive by other pattern matching for structural descent. so your call

    Strategy' ((X ∷ Xf) , inl _ , h)
    --> Strategy' (Xf x , h x)

    is applying Strategy' to a pair with (-1), i.e. decreasing, first component but ?, i.e. unknown, second component (h is not available, which is why the error message says Strategy' ((_ ∷ Xf) , inl _ , _)), which is overall a single pair argument with unknown relationship to the corresponding pattern, so the function call has no decreasing argument. in the two-argument version, you have a decreasing argument Xf _ followed by an unknown argument h _, and it's fine to have unknown arguments in the argument list, as long as one is decreasing.

    @de_Jong_Tom @totbwf

    💬 2🔄 0⭐ 0
  • 💬 0🔄 0⭐ 0
  • Martin EscardoMartinEscardo@mathstodon.xyz
    Oct 16, 2026, 5:13 PM

    @amy

    Thanks for the explanation. It is still disconcerting, both in Agda and Mikan, that currying versus uncurrying makes a difference for termination checking.

    Also, it is bad for modularity.

    But, yes, I understand the implementation issue - thanks!

    @de_Jong_Tom @totbwf

    💬 1🔄 0⭐ 0
  • Amélia Liao 🍊😈amy@types.pl
    Oct 16, 2026, 6:07 PM

    @MartinEscardo I commiserate, but somewhat unfortunately "make termination more accepting of [X syntactic transformation]" tends to devolve into "make termination more accepting of ⊥", like the old with-inlining transformation. There was some dead code in the termination checker for "matrix-shaped orders", which would allow componentwise comparison of record values against record patterns, but, well, it was never finished, so we just axed it.

    I'm planning to fix our documentation to call out cases like this, but there's so much to fix with the documentation that I'm stuck figuring out where to even start. For now I would offer the informal heuristic that "recursive calls must be made 'on' top-level arguments to the function, whose types can be seen to be inductive from the function's signature."

    @de_Jong_Tom @totbwf

    💬 0🔄 0⭐ 0