Strategies for dealing with partial information

[robrix]

We won’t always have all of the information available for a program. A partial (hah) list of conditions which can and will cause this:

• it may be ambiguous what the entry point(s) for a program are
• libraries don’t have entry points at all
• we might not know which source files are a part of which program if we don’t know about e.g. the build/package system
• we might not be able to resolve dependencies properly
• closed-source dependencies are a thing
• if we don’t know the environment a program is run in, we might not know how to resolve even local modules
• code can live in databases and networks that we don’t have access to
• there might be OS-specific code that we won’t have access to
• there might be a syntax error in a file
• there might be a parser, assignment, or analysis bug preventing us from evaluating a file
• user code may be ill-typed or buggy

Since we’re generally using approximate techniques, we will often be able to provide functionality proportional to the amount of information available to us—partial information should mean partial functionality, not zero functionality.

A brief and incomplete catalogue of strategies we can apply for this purpose:

• Use the information we do have to build up a picture of the information we don’t, à la typed holes in ghc, for example by using unification to guess the types of unknown terms.
• More generally, modelling a problem using constraints may allow us to resolve a solution precisely where we have sufficient information, and fall back gracefully to incomplete solutions where we do not. Treating this compositionally, that might mean computing what a function will do modulo what some specific unknown term will do.
• Symbolic execution will allow us to model the evaluation of irreducible terms using the terms themselves. This is known to be possible using abstract definitional interpretation (it’s in the paper), and is a valuable tactic for evaluation modulo unknown values in general.
• Similar to the technique of representing divergent computation with a bottom value, we can represent unknown values concretely s.t. elimination of an unknown value yields an unknown value.
• Using our intermediate language might allow us to represent unknown values/error states as the continuation from some expected result.

[robrix]

📌