Type Slicing

[MaxCarroll0]

Interactive Type Slicing

Implementation of Type Slicing and Cast Slicing as per my undergrad dissertation.

Type and cast slicing foundations and future directions/plans are summarised in a more readable in a shorter form in this progress paper.

Type Slicing

A type slice highlights parts of a term in order to explain it's (synthesised or analysed type)

For any term, a type slice is a minimal term and immediate context around the term which retains the same type information. That is, with all 'irrelevant' sub-term which don't give any new type information being replaced with holes. In this implementation, non-local context (variable definition and type definitions) are also highlighted (giving intuitive code slices for typing assumption slices). See examples below referring to terms at the red cursor):

Decomposability

This information is stored incrementally based upon the structure of the type of the expression in question. It tracks the part of a slice that results in, for example, the argument of a function having a type of Int.

Planned UI

Context Inspector

• For any selected term, always show the synthesising type and analysing type (when in analysis mode).

Decomposability by type

• Click on the (syn/ana) types in the context inspector to display their slices, highlighting to un-omitted term
• Toggle any sub-term's presence in the slice to retrieve only the parts of slices relevant to specific parts of the type
• Double-click on compound type constructors as a shortcut to viewing just the sub-slice for that constructor itself (with all sub-terms de-selected)

Emphasised Highlighting root constructors of types

Emphasise the parts of slices that actually sourced a particular type atom or constructor in question. That is, consider that (fun x -> 0)(1) has type Int but must highlight both the function constructor and eliminators to be a valid slice, but the atom 1 is where the type actually originates, and is perhaps of greater interest, so should be emphasised.

Emphasised Highlighting of root constructors of types in sub-slices

Distinguish between purely structural elements of sub-slices, and those which are root constructors of the (of part of the) type being scrutinised in the sub-slice. For example, a function may be a root constructor sourcing part of the type information, and must be present structurally to produce a valid slice, but might not actually be part of the part of the type being scrutinised, e.g. ? -> (? -> ?) when selecting the output function.

Un-emphasised parts could be omitted from highlighting in general by default. They likely just add noise to the slices with little non-trivial information.

Static Error Slices

• Show all inconsistent types in the context inspector.
• Highlight the inconsistent sub-parts of the involved types in red.
• Select parts of types as before, but in parallel between all types (where consistent).
• When selecting an inconsistent sub-part, only by default select the top-level (inconsistent) constructors. (As usual, emphasise the culprit root constructors)

Checklist

• Merge 'modeless'
• Separate analytic type logic and slicing into new 'Mode' module. PARTIALLY COMPLETE
• IMPORTANT: Refactor type slices to replace Typ.t, be a record type, adding helper functions to be usable in exactly the same way as Typ.t is currently
• Merge lastest dev updates
• Mathematical foundations.
• Preliminary implementation and UI.
• Proofs. PARTIALLY COMPLETE
• Remove dynamic witnesses code.
• Explicitly use ctx_used (as a list of slices)
• Implement type-based decomposable UI.
• Emphasise root constructors.
• Emphasise root constructors in sub-slices.
• Error slices UI. PARTIALLY COMPLETE
• Type slice substitution.
• Proofs that the slices are well-formed after substitution.
• Make list-cons type errors unbiased (as in branches and list literals). Type slicing can highlight the specific offending sub-terms.

Bugs & Tests

• Fix cast slicing selection in stepper.
• Rewrite existing tests. PARTIALLY COMPLETE
• Pass existing tests.
• Add tests for type slicing (each written in term-form of slices). Requires a framework to synchronise and structurally match term ID generation.
• Add tests for properties of type slicing. Requires reconstructing term-slices from ids in code slices.

Further Exploration

Decomposability by derivation & Tracking type eliminators

Type slices don't retain all information about derivations. For example, with type eliminators, lots of information is compressed into a single atomic part of the slice, as in (fun x -> 0)(1) having type Int so therefore not being decomposable (even though multiple rules were used in it's derivation).

Exploring how this information could be tracked and presented to the user and mathematical foundations for this would be of great use. In particular, how to integrate such a method seamlessly with the current type-based indexing.

Formal definition for emphasising parts of sub-slices

Allowing for proofs that a sub-term is always emphasised and proving and giving semantic justification of the concept.

Semantic Properties of Current Cast Slicing

Explore if the current propagation of type slice info throughout evaluation gives rise to any semantic properties. Especially, in relation to dynamic errors and 'dynamicness' of code. For example, how does this relate to blame?

Dynamic Program Slicing and its Relation to Cast Slicing

Type slicing can, to an extent, help understand why a cast was inserted during elaboration. A useful further feature would be slicing a minimal programs that produces a specific cast to help users understand why a cast was evaluated to. This could be based more generally upon 'Functional Programs that Explain their Work' which slices programs producing any part of a result.

In particular, in a minimal program producing some cast, how does the type slice information in this cast relate to the dynamic program slice itself.

Non-local Constraints and Inference

Possible integration with the form of inference-mimicking errors proposed by #1803.
Propagation of slicing within constraint solving may also be possible, but might not be possible to remain well-formed.

[MaxCarroll0]

Closing in favour of #2355

However, this branch did also implement dynamic type slices to explain dynamic type errors, which #2355 will not cover.