Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement new sort inference algorithm #3673

Merged
merged 52 commits into from
Dec 6, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
52 commits
Select commit Hold shift + click to select a range
40d7690
Initial implementation of constraint collection and compactification …
Scott-Guest Sep 27, 2023
8c1c057
Implement co-occurrence analysis and corresponding simplification.
Scott-Guest Oct 19, 2023
b4ff3d5
Merge remote-tracking branch 'origin/develop' into new-type-inference
Scott-Guest Nov 8, 2023
b78669d
Apply google style formatting to ParseInModule
Scott-Guest Nov 8, 2023
f748757
Applied formatting. Removed partially-implemented ambiguity logic
Scott-Guest Nov 8, 2023
e177dcd
Implement rough draft of cast insertion
Scott-Guest Nov 11, 2023
a12d545
Implement monomorphization
Scott-Guest Nov 13, 2023
ffec1b0
Add --z3-type-inference feature flag.
Scott-Guest Nov 13, 2023
d04a883
Actually hook new type inference algorithm into parser.
Scott-Guest Nov 14, 2023
0b4790a
Actually check --z3-type-inference flag. Change inference debug direc…
Scott-Guest Nov 15, 2023
2b4ed78
Merge remote-tracking branch 'origin/develop' into new-type-inference
Scott-Guest Nov 15, 2023
23d7bbd
Remove unused cast insertion modes from SortInferencer
Scott-Guest Nov 15, 2023
f23d825
Address IntelliJ warnings in Interface.scala
Scott-Guest Nov 15, 2023
375731f
Change logging to print whether each rule is inferred with Z3 or not.
Scott-Guest Nov 16, 2023
ea46d7b
Fix handling of function rules to prevent widening.
Scott-Guest Nov 16, 2023
96c2e9a
Track if the inferred term is a direct child of a #RuleContent or #Ru…
Scott-Guest Nov 17, 2023
94f7077
Improve error messages. Various bug fixes.
Scott-Guest Nov 22, 2023
70925be
Add missing copyright comments.
Scott-Guest Nov 22, 2023
04812a8
Apply scalafmt with 100 column width.
Scott-Guest Nov 24, 2023
2dd8177
Fix all IntelliJ warnings.
Scott-Guest Nov 24, 2023
e794277
Remove id from ProductionReference and store in Map instead.
Scott-Guest Nov 24, 2023
9e7ab11
Merge remote-tracking branch 'origin/develop' into new-type-inference
Scott-Guest Nov 24, 2023
2bd8b49
Merge remote-tracking branch 'origin/tree-nodes' into new-type-inference
Scott-Guest Nov 25, 2023
3ef8a8b
Add option to run both Z3 and SimpleSub algorithms then compare results.
Scott-Guest Nov 27, 2023
c5a44e8
Removed scala code and refactored accordingly.
Scott-Guest Nov 28, 2023
c502bcb
Improve documentation and naming.
Scott-Guest Nov 28, 2023
62ea7c8
Merge remote-tracking branch 'origin/develop' into new-type-inference
Scott-Guest Nov 28, 2023
40c1631
Fix formatting due to difference between CI and IntelliJ version
Scott-Guest Nov 28, 2023
6021754
Add missing copyrights
Scott-Guest Nov 28, 2023
ff291bf
Set default type inference mode to SimpleSub
Scott-Guest Nov 28, 2023
ab653f8
Merge branch 'develop' into new-type-inference
Scott-Guest Nov 28, 2023
2325ef8
Remove commented out debug code.
Scott-Guest Nov 28, 2023
e64bda8
Move sort inference write-up into docs/developers
Scott-Guest Nov 28, 2023
2a3f489
Add copyright header to doc
Scott-Guest Nov 28, 2023
870b529
Make Variable a record as the contained SortVariable now ensures that…
Scott-Guest Nov 29, 2023
5d208d5
Improve documentation and comments.
Scott-Guest Nov 29, 2023
939c658
Fix small bug in simplification where already optimized out variables…
Scott-Guest Nov 29, 2023
282ba57
Merge branch 'develop' into new-type-inference
Scott-Guest Nov 29, 2023
a60aa74
Restructure conditional TypeInferenceMode.CHECKED assertion.
Scott-Guest Nov 30, 2023
172050e
Remove HashSet double brace initialization
Scott-Guest Nov 30, 2023
9d36065
Improve documentation
Scott-Guest Nov 30, 2023
87bb328
Make use of enhanced instanceof check where applicable.
Scott-Guest Nov 30, 2023
0731f4f
Add further explanation of why MonomorphizationError has a poor error…
Scott-Guest Nov 30, 2023
b1965f7
Merge branch 'develop' into new-type-inference
Scott-Guest Nov 30, 2023
cef8679
Disable SimpleSub by default, but enable it in ktest.mak and ktest-fa…
Scott-Guest Dec 1, 2023
1a16dfc
Merge remote-tracking branch 'origin/develop' into new-type-inference
Scott-Guest Dec 1, 2023
2f282d2
Set the default in ParseInModule rather than KompileOptions so that i…
Scott-Guest Dec 1, 2023
402de1a
Fix bounds computation to allow us to infer parser sorts when they ar…
Scott-Guest Dec 2, 2023
bbde842
Add K as upper bound upon variable creation rather than special casin…
Scott-Guest Dec 2, 2023
536db01
Temporarily re-enable CHECKED to ensure CI still passes
Scott-Guest Dec 2, 2023
ff0eed3
Merge remote-tracking branch 'origin/develop' into new-type-inference
Scott-Guest Dec 6, 2023
a7e7aa7
Turn feature off for merge
Scott-Guest Dec 6, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
216 changes: 216 additions & 0 deletions docs/developers/sort_inference.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,216 @@
---
copyright: Copyright (c) Runtime Verification, Inc. All Rights Reserved.
---

# Design
The overall design of the new sort inference algorithm (`SortInferencer.java`) is based on the paper [The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy](https://infoscience.epfl.ch/record/278576) by Lionel Parreaux. We summarize the relevant parts below, but it's a short and enlightening paper that's worth reading if you want a deeper understanding.

## SimpleSub Summary
The SimpleSub paper describes a type inference algorithm for a lambda calculus with sub-typing. The type system is akin in expressiveness to something like Java-generics, i.e., permitting type variables `𝛼` with bounds `L <: 𝛼 <: U` (`super` and `extends` in Java).

Notably though, it captures this expressiveness with a very simple type semantics, enabling inferred subtyping constraints to be efficiently reduced to constraints on type variables (e.g. by mutating a type variable's sub-/super-type bounds throughout the inference process). As well, the results are expressed using "set-theoretic" types, which allow the type constraints to be recorded in an indirect, compact form while also making certain type-simplifications more obvious.

The inferred types have the following syntax
```
𝜏 ::= primitive // built-ins
| 𝜏 → 𝜏 // functions
| { 𝑙0 : 𝜏 ; ...; 𝑙𝑛 : 𝜏 } // structurally-typed records (won't be relevant for us)
| 𝛼 // type variables
| ⊤ // top type which is a supertype of all others
| ⊥ // bottom type which is a subtype of all others
| 𝜏 ⊔ 𝜏 // type unions / joins
| 𝜏 ⊓ 𝜏 // type intersections / meets
| 𝜇𝛼.𝜏 // recursive types (won't be relevant for us)
```
which is additionally subject to a *polarity* restriction. Informally, for a type `𝜏` which is a syntactic subcomponent of some other type `T`, the polarity of `𝜏` is
- *negative*, if `𝜏` describes a value given as an input to a term with type `T`
- *positive*, if `𝜏` describes a value produced by a term with type `T`

As a concrete example, in a type like `(𝜏0 → 𝜏1) → 𝜏2`,
- `𝜏2` is positive, as the term produces the value of type `𝜏2` as an output
- `𝜏0 → 𝜏1` is negative, as the value of this type is given as an input to the term
- `𝜏1` is negative, as the value of this type is also given as an input to the term (indirectly via the input function `𝜏0 → 𝜏1`)
- `𝜏0` is positive, as the term itself must produce this value in order to call the input function `𝜏0 → 𝜏1`

More formally, we define the type as a whole to be positive, and say
- `𝜏` is negative if either
- it occurs as the left part of an arrow `𝜏 → 𝜏'` where `𝜏 → 𝜏'` is itself positive, or
- it occurs as the right part of an arrow `𝜏' → 𝜏` where `𝜏' → 𝜏` is itself negative
- `𝜏` is positive otherwise

The polarity restriction on our type syntax then requires that
- type intersections `𝜏 ⊓ 𝜏` may only occur in negative position
- type unions `𝜏 ⊔ 𝜏` may only occur in positive position

To understand the motivation for this restriction, consider the subtyping constraints in a program and observe that
- if a type `𝜏` is negative, then it corresponds to an upper bound - the term requires a `𝜏` as input, and therefore can accept any sub-type of `𝜏`
- if a type `𝜏` is positive, then it corresponds to a lower bound - the term produces a `𝜏` as output, which can then be used at any place where some supertype of `𝜏` is expected

Informally then, the polarity restriction enforces that type intersections can only be used for upper bounds and type unions can only be used for lower bounds. In fact, there is an exact correspondence, as conversely any upper/lower bounds can always be encoded by a type intersection/union:
- `𝜏 <: 𝜏1 and 𝜏 <: 𝜏2 iff 𝜏 <: 𝜏1 ⊓ 𝜏2`
- `𝜏1 <: 𝜏 and 𝜏2 <: 𝜏 iff 𝜏1 ⊔ 𝜏2 <: 𝜏`

In total then, any type variable with bounds `L <: 𝛼 <: U` can be encoded as a set-theoretic type by
- replacing every negative instance of `𝛼` with `𝛼 ⊓ U`
- replacing every positive instance of `𝛼` with `𝛼 ⊔ L`

Conversely, any set-theoretic type subject to the polarity restriction can be converted back to type variables with bounds by iteratively applying this process in reverse, i.e.,
- replacing every intersection involving a type variable `𝛼 ⊓ U` with `𝛼` and recording the bound `𝛼 <: U` (introducing a fresh type variable for intersections involving only concrete types)
- replacing every union involving a type variable `𝛼 ⊔ L` with `𝛼` and recording the bound `L <: 𝛼` (introducing a fresh type variable for unions involving only concrete types)

For example, consider a term like
```
𝜆𝑥 . { L = 𝑥 − 1 ; R = if 𝑥 < 0 then 0 else 𝑥 }
```
where `nat <: int`, `- : int → int → int`, and `0 : nat`.

Prior to some simplification passes, SimpleSub will infer the type
```
𝛼 ⊓ int → { L : int ; R : 𝛽 ⊔ nat ⊔ 𝛼 }
```
which corresponds to the Java-esque type
```
⟨𝛼 extends int, 𝛽 super nat | 𝛼⟩(𝛼) → { L : int ; R : 𝛽 }
```
After simplification, SimpleSub will produce the final type
```
𝛼 ⊓ int → { L : int ; R : nat ⊔ 𝛼 }
```
which corresponds to the Java-esque type
```
⟨𝛼 super nat extends int⟩(𝛼) → { L : int ; R : 𝛼 }
```

### Inference Algorithm
With this background understood, the actual algorithm is quite simple. Below, I provide the algorithms from the paper in Scala with all the parts that are irrelevant to us removed (namely records, let-bindings, and recursive types).

Take our AST as follows:
```
enum Term {
case Lit (value: Int)
case Var (name: String)
case Lam (name: String, rhs: Term)
case App (lhs: Term, rhs: Term)
}
```
The first step is to produce a `SimpleType` which directly records bounds for each variable:
```
enum SimpleType {
case Variable (st: VariableState)
case Primitive (name: String)
case Function (lhs: SimpleType, rhs: SimpleType)
}

class VariableState(var lowerBounds: List[SimpleType],
var upperBounds: List[SimpleType])
```
The algorithm proceeds straightforwardly, noting type constraints at each function application:
```
def typeTerm(term: Term)(implicit ctx: Map[String, SimpleType]): SimpleType = term match {
case Lit(n) => Primitive("int")
case Var(name) => ctx.getOrElse(name, err("not found: " + name))
case Lam(name, body) =>
val param = freshVar
Function(param, typeTerm(body)(ctx + (name -> param)))
case App(f, a) =>
val res = freshVar
constrain(typeTerm(f), Function(typeTerm(a), res))
res
}
```
The constrain function propagates the newly found sub-typing constraint in a manner that ensures coherence with all previously recorded constraints:
```
def constrain(lhs: SimpleType, rhs: SimpleType)
(implicit cache: MutSet[(SimpleType, SimpleType)]): Unit = {
if (cache.contains(lhs -> rhs)) return () else cache += lhs -> rhs
(lhs, rhs) match {
case (Primitive(n0), Primitive(n1)) if subtype(n0, n1) => () // nothing to do
case (Function(l0, r0), Function(l1, r1)) =>
constrain(l1, l0); constrain(r0, r1)
case (Variable(lhs), rhs) =>
lhs.upperBounds = rhs :: lhs.upperBounds
lhs.lowerBounds.foreach(constrain(_, rhs))
case (lhs, Variable(rhs)) =>
rhs.lowerBounds = lhs :: rhs.lowerBounds
rhs.upperBounds.foreach(constrain(lhs, _))
case _ => err("cannot constrain " + lhs + " <: " + rhs)
}}
```
Once the `SimpleType` is inferred, we then go through the process described before of encoding the typing constraints as unions or intersections of the bounds. The end result is a `CompactType`, which denotes either a union or intersection of its contained types depending on the polarity where it occurs:

```
case class CompactType(vars: Set[TypeVariable],
prims: Set[PrimType],
fun: Option[(CompactType, CompactType)])
```
The implementation of the compact function is straightforward and omitted here.

We then perform two simplifications on these `CompactTypes` to remove unnecessary parametricity. We say that two type variables *co-occur* if they appear in the same union or intersection. The two simplifications are then as follows:

- If a type variable `𝛼` always co-occurs positively with some other type variable `β` and vice-versa, then `𝛼` and `β` can be unified. The same applies for negative occurrences. For example, the obvious type for an `if-then-else` function `bool → 𝛼 → β → 𝛼 ⊔ β` is in fact equivalent to `bool → 𝛼 → 𝛼 → 𝛼`.

- If a type variable `𝛼` always co-occurs both positively and negatively with some other type `T`, then `𝛼` can be removed. For example, `𝛼 ⊓ Int → 𝛼 ⊔ Int` is the same as `Int → Int`

See the paper for an explanation of why these simplifications are justified.

The final step of the algorithm is to coalesce each `CompactType` into the final set-theoretic type syntax described initially. Ignoring recursive types, this is just an easy syntactic transformation, so we omit the implementation here (it's also unneeded for our use cases).

## From SimpleSub To Sort Inference

To begin, consider the simplified setting of terms without ambiguities or parametric sorts.

The conceptual translation from K `Term`s to the SimpleSub language is straightforward.

First, given `pr` a `ProductionReference` whose id is `prId`, sort is `S`, non-terminal sorts are `S1, ..., SK`, and items are `t1, ..., tK`, we note that the typing constraints it induces are the same as any function symbol, so we let
```
translateBody(pr) = prId translateBody(t1) ... translateBody(tK)
```
where
```
prId : S1 → ... → SK → S
```
is taken as a built-in in the SimpleSub language.

Then, given `t` any `Term` containing variables `x1, ..., xN`, define the translation
```
translate(t) = 𝜆x1. ... 𝜆xN. translateBody(t)
```

When we perform type inference on `translate(t)`, we will obtain a function type of the form `T1 → ... → TN → T`. This tells us that `x1 : T1`, ..., `xN : TN`, and, `term : T`, exactly as needed for sort inference!

There are a few final caveats, which can be easily addressed:
- In K, we do not actually have a complete type lattice, and the intersections and unions of sorts may not actually exist. If we produce a type with such non-existent sorts, it is simply a type error.
- We do not yet support parametric rules throughout K, and may not ever support bounds on parametric sort variables (although this is something to consider!). We can address this by just monomorphizing with every sort in the poset that satisfies the appropriate bounds for each variable. These different monomorphizations should correspond one-to-one with the different maximal models found in the Z3-based sort inference engine.
- Function, macro, and anywhere rules must be special-case. Conceptually, we can just think of these as a `ProductionReference` to some specialized `KRewrite` whose return sort is exactly the declared sort of the LHS.
- Strict casts require us to unify rather than introduce subtyping constraints.

### Ambiguities
To extend the idea above to handle ambiguities, we note that any parse tree can be divided into unambiguous sub-trees (which we call *slices* in the implementation). The high-level idea is to infer a type for each slice parametric over its contained ambiguities.

Explicitly, given `t` a `Term` thought of as a tree/AST, cut `t` at each ambiguity node. This will produce a number of sub-trees trees, each of whose root node is either the root of `t` or the direct child of some `Ambiguity` occurring in `t`, and each of whose leaves are either a `Constant` or `Ambiguity`.

Given such a slice `t` containing `Ambiguity` nodes with which we associate identifiers `amb1, ..., ambK`, and presuming our overall term contains the variables `x1, ..., xN`, let
```
translateSlice(t) = 𝜆amb1. ... 𝜆ambK. 𝜆x1. ... 𝜆xN. translateBody(t)
```
and extend `translateBody` as above with the rule
```
translateBody(ambi) = ambi x1 ... xN
```
The intuition here is that our translation shows that any `Term` corresponds to a SimpleSub function abstracted over all the contrained variables, so an ambiguity can just be represented as some function variable (whose concrete types are not yet known) which is applied to all these variables.

When we perform inference on `translateSlice(t)`, the resulting type will have the form
```
(A11 → ... → A1N → A1) → ... → (AK1 → ... → AKN → AK) → T1 → ... → TN → T`.
```
Here, each `Ai` indicates the expected type of the `Ambiguity` associated to the identifier `ambi`.

If an ambiguity's child does not itself contain ambiguities (as will always be true far enough down in the parse tree), we can "fold" that particular child into the type of the parent slice by simple function application, corresponding to choosing that child of the ambiguity for our final parse.

Specifically, let `t` be the term as above and `c` its child slice. We can infer the type of the function application `translateSlice(t) translateSlice(c)` and will be left with either a type error or a type of the form
```
(A21 → ... → A2N → A1) → ... → (AK1 → ... → AKN → AK) → T1' → ... → TN' → T'`.
```
which is the specialization of `translateSlice(t)`'s type when picking `c` as the value of the ambiguity.

We can use this process to then iteratively collapse the tree of slices along all possible paths, starting from the leaves upward. Those paths that encounter type errors during substitution are pruned, while the others are collected into a set of all possible parses along with their inferred types. Unfortunately, this is `O(2^N)` in the worst case, but the hope is that the actual factors involved will be small.
2 changes: 1 addition & 1 deletion k-distribution/include/kframework/ktest-fail.mak
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ TESTS?=$(wildcard $(DEFDIR)/*.md) $(wildcard $(DEFDIR)/*.k)
KOMPILE_BACKEND?=llvm
KAST_TESTS?=$(wildcard ./*.kast)

KOMPILE_FLAGS+=--no-exc-wrap
KOMPILE_FLAGS+=--no-exc-wrap --type-inference-mode checked
KPROVE_FLAGS+=--no-exc-wrap
KRUN_FLAGS+=--no-exc-wrap

Expand Down
2 changes: 1 addition & 1 deletion k-distribution/include/kframework/ktest.mak
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ ifeq ($(UNAME), Darwin)
KOMPILE_FLAGS+=--no-haskell-binary
endif

KOMPILE_FLAGS+=--no-exc-wrap
KOMPILE_FLAGS+=--no-exc-wrap --type-inference-mode checked
KPROVE_FLAGS+=--no-exc-wrap
KRUN_FLAGS+=--no-exc-wrap

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
[Error] Inner Parser: Unexpected sort Int for term parsed as production syntax {Sort} Sort ::= Sort "=>" Sort [klabel(#KRewrite), symbol]. Expected: Bool
[Error] Inner Parser: Sort of variable X inferred as greatest lower bound of [Bool, Int], but no such bound exists.
Source(wideningMacro.k)
Location(8,10,8,25)
8 | rule #bar ( X ) => X
Expand Down
26 changes: 22 additions & 4 deletions kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java
Original file line number Diff line number Diff line change
Expand Up @@ -441,7 +441,11 @@ private Definition resolveConfigBubbles(Definition def) {
ParseCache cache = loadCache(configParserModule);
try (ParseInModule parser =
RuleGrammarGenerator.getCombinedGrammar(
cache.module(), profileRules, files, options.debugTypeInference)) {
cache.module(),
profileRules,
files,
options.debugTypeInference,
options.typeInferenceMode)) {
// each parser gets its own scanner because config labels can conflict with user
// tokens
parser.getScanner(globalOptions);
Expand Down Expand Up @@ -509,7 +513,8 @@ private Definition resolveConfigBubbles(Definition def) {
gen.getConfigGrammar(module),
profileRules,
files,
options.debugTypeInference)
options.debugTypeInference,
options.typeInferenceMode)
.getExtensionModule();
Set<Sentence> configDeclProductions =
stream(module.localSentences())
Expand Down Expand Up @@ -550,7 +555,14 @@ private Definition resolveNonConfigBubbles(
ParseCache cache = loadCache(ruleParserModule);
try (ParseInModule parser =
RuleGrammarGenerator.getCombinedGrammar(
cache.module(), profileRules, false, true, files, options.debugTypeInference, false)) {
cache.module(),
profileRules,
false,
true,
files,
options.debugTypeInference,
options.typeInferenceMode,
false)) {
Scanner scanner;
if (deserializeScanner) {
scanner = new Scanner(parser, globalOptions, files.resolveKompiled("scanner"));
Expand Down Expand Up @@ -582,14 +594,19 @@ private Module resolveNonConfigBubbles(Module module, Scanner scanner, RuleGramm
try (ParseInModule parser =
needNewScanner
? RuleGrammarGenerator.getCombinedGrammar(
cache.module(), profileRules, files, options.debugTypeInference)
cache.module(),
profileRules,
files,
options.debugTypeInference,
options.typeInferenceMode)
: RuleGrammarGenerator.getCombinedGrammar(
cache.module(),
scanner,
profileRules,
false,
files,
options.debugTypeInference,
options.typeInferenceMode,
false)) {
if (needNewScanner) parser.getScanner(globalOptions);
parser.initialize();
Expand Down Expand Up @@ -789,6 +806,7 @@ public Rule parseRule(CompiledDefinition compiledDef, String contents, Source so
true,
files,
options.debugTypeInference,
options.typeInferenceMode,
false)) {
parser.setScanner(new Scanner(parser, globalOptions, files.resolveKompiled("scanner")));
java.util.Set<K> res =
Expand Down
20 changes: 19 additions & 1 deletion kernel/src/main/java/org/kframework/kompile/KompileOptions.java
Original file line number Diff line number Diff line change
Expand Up @@ -241,7 +241,25 @@ public String syntaxModule(FileUtil files) {

@Parameter(
names = "--enable-kore-antileft",
description = "Enable generation of legacy antileft priority predicates ",
description = "Enable generation of legacy antileft priority predicates.",
hidden = true)
public boolean enableKoreAntileft;

public enum TypeInferenceMode {
Z3,
SIMPLESUB,
CHECKED,
// We use an explicit DEFAULT option here so that ParseInModule can set a default which
// applies even for those codepaths that don't rely on KompileOptions
DEFAULT,
}

@Parameter(
names = "--type-inference-mode",
description =
"Choose between the Z3-based and SimpleSub-based type inference algorithms, or run both"
+ " and check that their results are equal. Must be one of "
+ "[z3|simplesub|checked|default].",
hidden = true)
public TypeInferenceMode typeInferenceMode = TypeInferenceMode.DEFAULT;
}
Loading