Type slicing v2

[MaxCarroll0]

Summary

This adds query-driven polymorphic type slicing to Hazel. It is an approximation of this paper.

When selecting a term, it has a synthesised type and (sometimes) an expected type. Slicing allows us to omit parts of either of these types to form a query, and retrieves a fragment of the term and respectively the surrounding context around the term which explains the queried part of the type (omitting regions by ID).

Formally, if we place holes at omitted locations, a sliced program should synthesise / expect a type at least as strong as we queried at the term we were selecting.

Further, it also calculates subparts of the types each variable/type constructor needs. i.e. a slice of the typing context at the term.

Type	Definition	What it holds
gamma	VarMap.t_(Typ.t)	the assumptions: one refined type per free name the slice still needs
sty (sliceable type)	{shape, dispatch, finalize}	a node's own type, plus a lazy query => result
result	{omitted, gamma, psi, context, ana}	a slice: omitted ids, gamma, the sliced type psi, and the minimal context/analysis type it still needs
child_mode	Keep, Omit, or Source	which let operator tagged a sub-term's recursion

The implementation is lazy, and does not require full reconstructing a full info map, though slicing follow the same flow as type checking, so has similar asymptotics.

It intentionally piggybacks upon the existing statics system. Slicing mechanism follows the same dataflow as slicing in most cases (reversed for binders), and tries to integrate into it with minimal changes to the type checking infrastructure.

This should mean that you can write new type checking rules mostly how you would before, then simply annotate how slicing works on top. I expect that you should generally be able to get most slicing behaviour correct using just a few heuristics (below). The only slight differences are reworking the interface to type matching functions (arrow_tolerant etc.) and CoCtx (which now tracks constructors and aliases too).

Adding to Statics.re

1. Write a new typing rule normally first, using ordinary let bindings and type formers.
2. Check your typing rules etc. etc.
3. Annotate recursive bindings (let ... = go(...)) with custom let operators which act as heuristics describing how each sub-term’s type contributes to the result.

Type formers

Use a MatchedTyp former to describe how types can be matched and rebuilt, i.e. projections from a product, and building a1 product.

List Cons Example

let* (hd, hd_elab, m) =
  go(~ana=MatchedTyp.list_tolerant(ctx, ana), hd, m);

let& (tl, tl_elab, m) =
  go(~ana=List(hd.ty) |> Typ.temp, tl, m);

The head supplies the list's element type (let*): the query is matched against the List former, routed in to hd, and the result is rebuilt from what comes back. The tail is only checked (let&), since a cons cell's type already comes from its head — slicing tl further couldn't add anything the head didn't already supply.

Binding Example

let (p_syn, _, _) =
  go_pat(~co_ctx=CoCtx.empty, ~ana=syn, p, m);

let$ (def, def_elab, m) =
  go(~ana=p_syn.ty, def, m);

let* (body, body_elab, m) =
  go(~ctx=p_ana_ctx, ~ana, body, m);

let@ (p_ana, p_elab, m) =
  go_pat(~co_ctx=body.co_ctx, ~ana=def.ty, p, m);

Use let$ for definitions behind bindings. Use let* for any expression whose type feeds the result directly, whether it's one component of something larger or, as with body here, the whole thing unchanged. Use let@ for final slices on patterns.

Alternative branches

Use let& for subterms which are type checked against (e.g. conditional in an if statement). Use let+ for types which are met to compute an overall type (e.g. branches in if statements):

let& (cond, cond_elab, m) =
  go(~ana=Atom(Bool) |> Typ.temp, cond, m);

let+ (cons, cons_elab, m) = go(~ana, cons, m);
let+ (alt, alt_elab, m) = go(~ana, alt, m);

Each branch receives the query remaining after the preceding branches. Their types are still combined using
Hazel’s existing Typ.meet operations.

Co-contexts

A co-context (CoCtx.t) is the dual of a context: a map from variable name to every use of it in scope, each entry carrying the id and expected type of that use site. Ordinary type checking already compares it against the context to find free and unused variables without a second pass over the term; slicing reuses it unchanged, except an entry can now come from a constructor or alias use as well as a variable, since a slice needs the same free/unused reasoning to decide which constructors and aliases it must keep.

Operator reference

Operator	Use	Example
let*	An expression or pattern supplies the result type, or one component of it when the result is built from several. The whole-type case is just this with a single component.	A list element supplies the list’s element type; the body of let p = d in body supplies its type whole.
let&	A sub-term is checked (so does not supply the result type).	An if condition.
let$	Definitions behind bindings (defs, scrutinees)	The definition in a let.
let@	On pattern bindings themselves (final call only if you call multiple times)	A function parameter.
let+	A branch is an alternative source of the same result type.	An if branch.

When the sub-term being recursed is actually a TYPE, you double the symbols: i.e. let$$ is used for type aliases definitions.

There are also some more specific adhoc binders or combinations:

Operator	Use	Example
let^?	A sub-term supplies the complete type but may be pruned for a shape only query. Requires a former.	List concatenation.
let&>	As let&, with its expected query supplied by an explicit source.	An ascribed expression checked by its annotation.
let@+	A pattern binds names for one corresponding alternative.	A match pattern and branch.
let^*	The result is a named component projected from a sub-term’s type.	The codomain of a function application.
let^>	A pattern supplies the complete type and is checked from an explicit type source.	An ascribed pattern.

TODO: have fewer adhoc binders.

Architecture

• Lazily computed
• Extensible, due to not using explicit matches on type functions (at least in the direct slicing code)
• Slicing direction is reversed automatically by the use of operators (i.e. binders using let$ reverse the direction)

Testing strategy

• Statics.Slicing.Synthesis: ordinary slicing of synthesis typing rules
• Statics.Slicing.Analysis: analysis slicing of subterms querying the expected type.
• Statics.Slicing.Binding: binding operators (reverse slicing flow). This also tests the gamma storing the typing context slices.
• Statics.Slicing.ExtendedExamples covers larger examples, including subterms in synthesis position, and larger branching code.
• Statics.Slicing.InvalidQuery checks missing focus, wrong focus sort, and incompatible query shape exceptions.
• Type formers (MatchedTyp) aren't tested in isolation; they're exercised as part of a full rule, through the Synthesis/Analysis/Binding suites above.
• TypeSlicing.UI slicing is linked up to a overlay to fold away omitted regions correctly in the UI
• Property Tests: Validity (slices actually produce the same types), and Monotonicity (smaller queries produce monotonically smaller and consistent slices).

[codecov]

Codecov Report

❌ Patch coverage is 48.28660% with 498 lines in your changes missing coverage. Please review.
✅ Project coverage is 51.17%. Comparing base (f454912) to head (27d08be).

Files with missing lines	Patch %	Lines
src/web/app/inspector/CursorInspector.re	39.34%	333 Missing ⚠️
src/web/app/explainthis/ExplainThis.re	36.20%	37 Missing ⚠️
src/web/app/editors/code/CodeEditable.re	3.57%	27 Missing ⚠️
src/language/statics/Info.re	4.54%	21 Missing ⚠️
src/language/statics/Statics.re	87.50%	18 Missing ⚠️
src/haz3lcore/lang/MakeTerm.re	66.66%	11 Missing ⚠️
src/language/statics/SliceReconstruct.re	79.16%	10 Missing ⚠️
src/web/app/editors/code/Code.re	0.00%	9 Missing ⚠️
src/web/app/editors/code/ContextMenu.re	0.00%	7 Missing ⚠️
src/web/debug/DebugConsole.re	0.00%	7 Missing ⚠️
... and 7 more

Additional details and impacted files

@@                    Coverage Diff                    @@
##           parameterized-types-4    #2355      +/-   ##
=========================================================
- Coverage                  51.41%   51.17%   -0.24%     
=========================================================
  Files                        297      366      +69     
  Lines                      40723    47588    +6865     
=========================================================
+ Hits                       20937    24354    +3417     
- Misses                     19786    23234    +3448     

Files with missing lines	Coverage Δ
src/haz3lcore/projectors/ProjectorPerform.re	25.43% <100.00%> (+22.71%)	⬆️
src/language/statics/CustomStatics.re	90.56% <ø> (ø)
src/language/statics/StaticsSlice.re	80.18% <ø> (ø)
src/language/term/Typ.re	59.36% <100.00%> (+1.33%)	⬆️
src/web/app/common/RefractorView.re	0.00% <ø> (ø)
src/haz3lcore/TyDi/ErrorPrint.re	14.73% <0.00%> (-0.08%)	⬇️
src/haz3lcore/derived/CachedStatics.re	52.83% <90.90%> (+8.38%)	⬆️
src/haz3lcore/pretty/ExpToSegment.re	62.80% <83.33%> (+1.59%)	⬆️
src/haz3lcore/zipper/action/Indicated.re	70.87% <93.33%> (+3.85%)	⬆️
src/web/app/editors/decoration/CaretDec.re	0.00% <0.00%> (ø)
... and 12 more

... and 97 files with indirect coverage changes

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.