Struct Subst

Source

pub struct Subst { /* private fields */ }

Expand description

A unification variable’s binding, shared so that unifying in one place is visible everywhere.

Implementations§

Source §

pub fn resolve(&self, t: &Ty) -> Ty

Fully apply the substitution — what diagnostics and the emitted Core see.

Source

pub fn resolve_row(&self, r: &Row) -> Row

Expand a row through its variable bindings, to a fixed point.

The seen set is not a safety net; it is the semantics. A definition’s row variable can be bound to a row that mentions itself — that is what mutual recursion between two effectful functions is — and because a row is a union, stopping at an already-expanded variable computes exactly the least fixed point rather than diverging.

Source

pub fn bind_row(&self, v: RowVarId, r: Row)

Source

pub fn instantiate(&self, s: &Scheme) -> Ty

Instantiate a scheme with fresh type and row variables.

Source

pub fn instantiate_named(&self, s: &Scheme) -> (Ty, BTreeMap<Arc<str>, Ty>)

Subst::instantiate, and the fresh variable each named parameter became.

A bounded definition needs the map: def sort[T: Ord](xs: list[T]) is lowered with a dictionary parameter per method of Ord, and the call site can only say which impl to pass once it knows what this call’s T turned out to be. docs/39 §39.4.

Source

pub fn unify_join(&self, a: &Ty, b: &Ty) -> Result<Ty, Mismatch>

Unify two types that are alternatives rather than actual-and-expected, and return the type of whichever one runs.

Subst::unify is asymmetric on purpose: its first argument is the actual type and its second the expected one, and Subst::subsume_row leans on that so a function which does less than its context allows is accepted. The two branches of an if are neither. Making one of them the “expected” type of the other says that a branch returning identity — inferred pure, so its row is closed — is the standard the other branch has to meet, and the other branch returning a call’s result carries a row variable. A variable is not a subset of the empty row, so the two are reported as a conflict, with nothing missing to name:

error[B0320]: the two branches may not perform {} here

which is docs/25-benchmarks-and-expressiveness.md §25.6 item 6, and what exercise 1.43 costs. The answer is the one every row-typed language reaches: the alternatives do not meet each other, they both flow into a fresh row, and the result performs whatever either of them might. Sound in the direction §3.2 requires — the join contains both branches’ atoms, so an effect can never be lost — and it leaves a free tail, exactly as a written function type does, so a later context may widen it again.

Source

pub fn unify(&self, a: &Ty, b: &Ty) -> Result<(), Mismatch>

Source

pub fn subsume_row(&self, actual: &Row, expected: &Row) -> Result<(), Mismatch>

Require actual ⊆ expected — the effect-row subsumption §3.1 permits and nothing else.

Rows are sets, so this is: whatever the actual row does, the expected row must already allow, or must have a variable free to absorb it. Concretely, three cases and no more:

everything the actual side does is already named on the expected side — nothing to do;
the expected side has a free row variable — bind it to the difference, leaving a fresh variable behind so a later call site can widen it again. This is what makes (a -> b ! e) accept a pure function at one call and an effectful one at the next;
the expected side is closed and lacks something — the rows genuinely differ, and that is the error.

The direction is the design. Equality would make a pure lambda fail to match (a -> b ! e) unless e were solved first, and would make the same higher-order function unusable at two call sites with different arguments. Subsumption over-approximates in one direction only: a definition’s inferred row may be a superset of what one call actually performs, which can cost a placement candidate but can never lose an effect.

Source