Mentions légales du service

Skip to content
Snippets Groups Projects

typed holes (with subterms) for shrinking

Merged SCHERER Gabriel requested to merge gscherer/inferno:typed-holes into master

A typed hole can have any type (it imposes no typing constraints on the context around it), and its subterms can have any type (the hole imposes no constraint on them).

This is the ultimate language construct to do type-preserving shrinking. When shrinking it is important to be able to remove subterms that do not participate to the error.

Holes with no subterms can be used to completely erase a term. Holes with subterms can be used to selectively erase parts of a term (for example, the application "t u" can be rewritten into the hole "...[t, u]", erasing only the application rule).

The MR also contains some independent improvements to the shrinking strategy; in particular convenient shrinking for products, which I hope to possibly upstream in QCheck directly.

Edited by SCHERER Gabriel

Merge request reports

Merge request pipeline #252002 passed

Merge request pipeline passed for eedfd95c

Approval is optional

Merged by SCHERER GabrielSCHERER Gabriel 3 years ago (Jun 10, 2021 4:19pm UTC)

Loading

Pipeline #258700 passed

Pipeline passed for e6953c62 on master

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Author Maintainer

    cc @omartino, @fpottier. This is something that I discussed with @omartino (I didn't know when we could implement it), and I would be interested in a high-level opinion from François; in particular I think the (hinted) relation to typed error slicing may be interesting.

    (I think that the relation is that we may be computing a minimal slice while shrinking (I'm not sure how to check it), but in an inefficient way as we retype each new term completely from scratch. It is completely fine in practice. I don't know how to do this more incrementally if we wanted to, given that we shrink terms starting from the leaves, instead of typing a partial term that gets more and more complete. Maybe we should try to complete a partial tree from the root to the leaves...)

  • SCHERER Gabriel changed the description

    changed the description

  • Author Maintainer

    For a concrete example of improved shrinking, I injected a bug in the application rule. Before this MR, our shrinked counter-example is

    fun x0 ->
      fun x1 -> x0 (let (x2, x3) = x1 in fun x4 -> (fun x5 -> x3) x3)

    with typed holes (and some improvements to shrinking)

    ...[] (fun x5 -> ...[])

    where ...[] is the syntax for holes without subterms.

  • This looks good to me. I am not sure about the relation with minimal type error slicing. Does "minimal type error slicing" mean "keep only the constraints that participate in an error", or does it mean "keep only the AST nodes that participate in an error", or something else?

  • Author Maintainer

    There is an explicit connection between these two notions in Haack and Wells paper ("Type error slicing in implicitly typed higher-order languages", 2004): from a set-of-locations obtained from a minimal-set-of-constraints, they show how to determine a program-with-holes that is ill-typed, and minimal in the sense that any programs with more holes is well-typed.

    (For the record: Olivier and myself thought of introducing typed holes (without subterms/arguments) during a discussion about shrinking. When I asked around if holes had been used for shrinking before, Neelakantan Krishnaswami pointed to their use in the Haack and Wells. This inspired me to add subterm arguments to our holes as well.)

  • SCHERER Gabriel mentioned in commit e6953c62

    mentioned in commit e6953c62

Please register or sign in to reply
Loading