Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
35 commits
Select commit Hold shift + click to select a range
484eafb
WIP
LPTK Oct 15, 2026
45842c6
Compute runtime erased types from completed resolution shapes
codex Oct 15, 2026
fca467d
WIP
LPTK Oct 15, 2026
0629de9
Shorten i32 constants in erasure regressions
codex Oct 15, 2026
1f5390b
Eliminate casts made redundant by IR simplification
codex Oct 15, 2026
f853f10
Preserve function representations when lowering lambdas
codex Oct 15, 2026
551e4a8
Preserve representations across deforestation rewrites
codex Oct 15, 2026
3caffd0
Preserve checked arguments when propagating partial calls
codex Oct 15, 2026
35fa0bd
Fuse constructors through casts proved by flow analysis
codex Oct 15, 2026
c6b0f63
Preserve existing spacing in Wasm regression tests
codex Oct 15, 2026
d41909e
Merge branch 'hkmc2' into compute-erased-types-from-shapes
codex Oct 18, 2026
b87501d
Address review of erased types computed from shapes
claude Oct 18, 2026
e5e6126
Update golden output for shifted internal-error line numbers
claude Oct 18, 2026
d710d52
Infer the representation of the temporary saved by `set … in`
claude Oct 19, 2026
eb47bae
Merge branch 'hkmc2' into compute-erased-types-from-shapes
codex Oct 19, 2026
8bfe6a3
Infer representations of mutable fields from their assignments
claude Oct 19, 2026
1b878f2
Declare mutable record fields with `mut`
claude Oct 19, 2026
c0af69c
Update golden output after rebasing mutable-field work
claude Oct 19, 2026
9539de3
test: cover values escaping through mutable record assignments
codex Oct 19, 2026
081891b
Fix mutable-field exposure and preserve read/write variance
codex Oct 19, 2026
632d227
test: verify both mutable record constraint directions
codex Oct 19, 2026
6cdba57
Merge optional-params and reconcile shape-based erasure
codex Oct 22, 2026
65660c4
Fix review regressions in exposure, overrides, and fusion
codex Oct 22, 2026
e997c04
Merge hkmc2 and preserve consolidated regression coverage
codex Oct 23, 2026
159f6c7
add tests
ychenfo Oct 17, 2026
aec9ed6
tweaks
ychenfo Oct 20, 2026
c43cf3d
keep constructors unfused in fields that cannot hold their fused form
ychenfo Oct 20, 2026
3ca8e62
type the temporary holding a fused nullary constructor's closure
ychenfo Oct 20, 2026
852c5b1
cast calls replacing fused matches into the enclosing result
ychenfo Oct 20, 2026
5fa7f42
copy functions at the instances whose types fusion changes
ychenfo Oct 20, 2026
65fb4b7
wip
ychenfo Oct 23, 2026
4d9026e
replace unproducible values that causes erased type error in flow-typ…
ychenfo Oct 23, 2026
b982195
update type for eta and dpe
ychenfo Oct 23, 2026
e1e4d60
test: reproduce deforestation error for unboxed returns
codex Oct 24, 2026
83440c8
Merge pull request #33 from ychenfo/compute-erased-types-from-shapes-…
LPTK Oct 26, 2026
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
104 changes: 101 additions & 3 deletions doc/reference.md
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,7 @@ true // Boolean literal
false // Boolean literal
() // Unit literal (empty tuple/record)
null // Null
undefined // Undefined
undefined // Undefined: an unspecified value (see Runtime Representations)
```

**String escape sequences:**
Expand Down Expand Up @@ -758,10 +758,15 @@ Modules cannot extend classes. Objects can extend classes.

```mlscript
{a: 1, b: 2} // immutable (frozen) record
mut {a: 1, b: 2} // mutable record
{mut a: 1, b: 2} // record whose field `a` is mutable
mut {a: 1, b: 2} // mutable record: all its fields are mutable
(a: 1, b: 2) // record in parentheses (same thing)
```

Only mutable fields can be assigned. Fields are immutable unless they are declared `mut` or
their whole record is mutable. A mutable record also makes mutable the fields it copies from
the records it spreads. A record spreading another one copies the current values of its fields.

### Field Access

```mlscript
Expand Down Expand Up @@ -1543,6 +1548,80 @@ candidate and a known candidate with an invalid operation, the known error is
still reported. Dynamic values also do not remove the need for an unambiguous
class or type identity in constructor patterns, class projections, or type references.

### Runtime Representations

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[Claude] As @LPTK asked, the two design decisions from my review are now explicit:

  • undefined is an unspecified value, and reading it back is undefined behavior. This is documented here, in the literal table above, and in Block.isUndefined.
  • Programs whose only problem is a misleading annotation are now rejected. This is documented here and in the Erasure class documentation.

This section also covers interface exposure, worksheets, overrides, and the builtin-operator approximation.


Compilation chooses a runtime *representation* for each slot that holds values: parameters,
results, fields, and variables. On the JavaScript backend, all values share one representation,
so representations mostly matter on the Wasm backend, where an `Int32` is an unboxed `i32` and
a class instance is a reference to the class's struct. A type annotation determines the
representation of its slot. With new resolution (`#lang(0.3.x)`), an unannotated slot takes the
representation of the values that resolution observes flowing into it:

```mlscript
private fun roundtrip(value) = value // `value` and the result are represented as `Int32`
roundtrip(wasm.i32.const(42))
```

A value is converted to the representation of each slot it flows into. Converting between
unrelated representations is a compilation error, whether the slot's representation is declared
or inferred, and so is a slot whose values have no common representation. This also rejects
programs whose only problem is a misleading annotation, which the JavaScript backend would run:

```mlscript
class Tree
class App(callee: Tree, argument: Tree)
fun mk(t: Tree) = App(t, 1 :: Nil) // error: a list is used at the representation of `Tree`

let value = wasm.i32.const(1)
set value = wasm.i64.const(2) // error: `Int32` and `Int64` have no common representation
```

Slots that can receive values from outside the compilation unit admit them: the unannotated
parameters of exposed definitions (see Resolution Interfaces) are inferred with unknown inputs.
Worksheet blocks are compiled one after the other, so without `#lang(strictResolution: true)`,
later blocks must use an earlier block's definitions with the representations inferred from that
block's own uses.

A mutable field holds its initializer and then the values assigned to it, through any receiver that
can be an instance of its class, so an unannotated mutable field takes the representation of all of
them. Since other compilation units can assign values to the mutable fields that a compilation unit
exposes, those must declare their types, as their representations must not depend on the values that
the compilation unit happens to assign to them:

```mlscript
private class Cell(mut val value) // `value` is represented as `Int32`
private fun reset(cell) = set cell.value = wasm.i32.const(0)
reset(Cell(wasm.i32.const(1)))

class Counter(mut val count) // error: `count` is exposed, so its type must be declared
class Counter(mut val count: Int) // ok
```

Mutable record fields (see Record Literals) can be assigned too, but cannot declare their types:
when exposed, they take the unknown representation. Through a record type declaring a mutable
field, the values it describes can be assigned values of that field's input type, which their own
fields therefore admit. Exposing a record also exposes values stored by assignments, including
through fields copied by a mutable spread: those values can be read by clients just like initializers.

An override shares the representations of the member it overrides. Its unannotated parameters
take the inherited parameters' representations, its annotated parameters must admit them (and,
on the Wasm backend, which compiles overrides with the overridden method's signature, match
them), and its results must fit the inherited result. A mismatch is a compilation error. Since
subclasses in other compilation units must implement an open member with its representations,
an open member whose parameters receive values from outside the compilation unit must annotate
the types of its parameters and result.

The builtin operators are not yet declared as overloaded functions: their results are approximated
from their operands. For example, the sum of two `Int`s is an `Int` (an overflow to `Infinity` is
not detected), and `+` with a `Str` operand is a `Str`. On the Wasm backend, which implements the
operators with dynamically typed runtime functions, their results are treated as unknown values.

`undefined` denotes an unspecified value of any representation. It can be stored in or passed to
any slot, but reading it back is undefined behavior: the JavaScript backend produces JavaScript
`undefined` (or `()` for a function returning it), while the Wasm backend may produce any value
of the slot's representation, such as `0` for an `Int32` or a null reference. Compiler-generated
placeholders, such as the arguments supplied for eliminated dead parameters, rely on this.

### Generic Type Parameters

Covariant, contravariant, invariant:
Expand Down Expand Up @@ -1609,7 +1688,26 @@ lookup still combines the fields of record intersections.

```mlscript
type Point = { x: Num, y: Num }
```
type Cursor = { mut position: Int }
type CursorView = { mut position: in Int out (Int | Str) }
```

The values that a record type describes can be assigned values of the input types of its mutable
fields through it, but not values of its other fields. In `{ mut f: in S out T }`, writes accept `S`
and reads expose `T`. Omitting `in` gives `Nothing` as the input; omitting `out` gives `Any` as the
output. `{ mut f: U }` uses `U` in both positions, while `{ f: U }` has only a read interface.

Field outputs are covariant and field inputs are contravariant. Thus `{ mut f: S } <: { mut f: T }`
contributes both `S <: T` for reads and `T <: S` for writes; `mut { f: S }` follows the same rule.
The two occurrences are interpreted separately before substituting type arguments:
for `type Cell[A] = { mut f: A }`, `Cell[in S out T]` exposes
`{ mut f: in S out T }`, not a single invariant occurrence of either bound. Enclosing negative
positions reverse these choices, just as for function inputs. Intersecting record interfaces
intersects their shared fields' output types and unions their input types. Assigning a callback
through a mutable field constrains it against the input type, independently of the read interface.

New resolution propagates these constraints for type-argument inference and callback checking.
It does not perform complete structural subtyping checks; InvalML does not yet support record types.

Under new resolution, recursive type aliases must be guarded: every recursive
cycle must pass through a record, tuple, function arrow, or nominal type.
Expand Down
33 changes: 33 additions & 0 deletions hkmc2/jvm/src/test/scala/hkmc2/ErasureInputsTest.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
package hkmc2
package semantics

import org.scalatest.funsuite.AnyFunSuite
import hkmc2.utils.*

/** Diff tests exercise representations. This checks the separate ownership property:
* consumers and later worksheet blocks cannot mutate completed observation snapshots.
*/
class ErasureInputsTest extends AnyFunSuite:
test("completed observations are isolated from worksheet and import consumers"):
given owner: Elaborator.State = new Elaborator.State
given defining: ResolutionContext = owner.newResolverState.context
val inputs = owner.newResolverState.erasureInputs
val symbol = VarSymbol(new syntax.Tree.Ident("value"))
val source = new TermShapeHost
inputs.register(symbol)(source.subscribeToShapes)
val initial = DynShape()
source.publish(initial)
defining.completeBlock(Term.UnitVal())
val snapshot = inputs.shapes(symbol)
val first = new Elaborator.State().newResolverState.context
val second = new Elaborator.State().newResolverState.context
val later = UnknownValueShape.at(Term.UnitVal())
val other = UnknownValueShape.at(Term.Lit(syntax.Tree.IntLit(1)))
source.publish(later)(using first)
source.publish(other)(using second)
source.publish(other)(using defining)
assert(source.currentShapes(using first).toSet == Set(initial, later))
assert(source.currentShapes(using second).toSet == Set(initial, other))
assert(source.currentShapes(using defining).toSet == Set(initial, other))
assert(snapshot == List(initial))
assert(inputs.shapes(symbol) == snapshot)
10 changes: 5 additions & 5 deletions hkmc2/jvm/src/test/scala/hkmc2/TypeRelationTest.scala
Original file line number Diff line number Diff line change
Expand Up @@ -214,8 +214,8 @@ class TypeRelationTest extends AnyFunSuite:
value.typeInterpretation = S(element.resolution)
val next = Term.UnitVal()
next.typeInterpretation = S(resolution)
val valueField = RcdField.signature(Term.Lit(Tree.StrLit("value")), value)
val nextField = RcdField.signature(Term.Lit(Tree.StrLit("next")), next)
val valueField = RcdField.signature(Term.Lit(Tree.StrLit("value")), value, false, N)
val nextField = RcdField.signature(Term.Lit(Tree.StrLit("next")), next, false, N)
val source: Term.Rcd = Term.Rcd(false, List(valueField, nextField))
resolution.publish(TypeShape.Record(source, List(valueField -> element.resolution, nextField -> resolution)))
DeclaredType(resolution, Map.empty, TypeSubstitution.empty, true)(N)
Expand Down Expand Up @@ -574,7 +574,7 @@ class TypeRelationTest extends AnyFunSuite:
val left = new TypeResolution(Term.UnitVal(), _ => fail("Unexpected type error"))
val right = new TypeResolution(Term.UnitVal(), _ => fail("Unexpected type error"))
def recursive(resolution: TypeResolution): Unit =
val next = RcdField.signature(Term.Lit(Tree.StrLit("next")), Term.UnitVal())
val next = RcdField.signature(Term.Lit(Tree.StrLit("next")), Term.UnitVal(), false, N)
val source: Term.Rcd = Term.Rcd(false, List(next))
resolution.publish(TypeShape.Record(source, List(next -> resolution)))
recursive(left)
Expand All @@ -584,10 +584,10 @@ class TypeRelationTest extends AnyFunSuite:
case (value: RecordTypeShape) :: Nil => value
case _ => fail("Expected one merged record")
val first = record(intersection)
val next = first.fields("next")
val next = first.fields("next").output
val saturated = record(next)
val counts = (left.inferenceHost.listeners.size, right.inferenceHost.listeners.size)
(1 to 1000).foreach: _ =>
assert(record(saturated.fields("next")) eq saturated)
assert(record(saturated.fields("next").output) eq saturated)
assert((left.inferenceHost.listeners.size, right.inferenceHost.listeners.size) == counts)
assert(h.state.allocatedTypeInstanceCount == 0)
67 changes: 53 additions & 14 deletions hkmc2/shared/src/main/scala/hkmc2/codegen/Block.scala
Original file line number Diff line number Diff line change
Expand Up @@ -374,7 +374,8 @@ end Block
object Block:
/** The union of the types returned from `block`, whose canonical form is their least upper bound.
*
* `N` means there are no returns; an untyped return contributes `Unknown` instead. Nested function, lambda,
* `N` means there are no constraining returns: `undefined` can inhabit any representation. Other untyped
* returns contribute `Unknown` instead. Nested function, lambda,
* and class bodies have their own returns and are excluded. All other returns count, including unreachable
* ones, since backends such as Wasm still validate their types.
*
Expand All @@ -385,7 +386,7 @@ object Block:
val types = Buffer.empty[ErasedValueType]
val collector = new BlockTraverserShallow:
override def applyBlock(b: Block): Unit = b match
case Return(res) => types += res.erasedValueType_!
case Return(res) => if !res.isUndefined then types += res.erasedValueType_!
case _ => super.applyBlock(b)
collector.applyBlock(block)
Option.when(types.nonEmpty)(ErasedType.Union.mk(types))
Expand Down Expand Up @@ -833,7 +834,13 @@ private[codegen] object InlinerBodySummary:

object FunDefn:
def withFreshSymbol(owner: Opt[InnerSymbol], sym: BlockMemberSymbol, params: Ls[LoweredParamList], body: Block)(configOverride: Opt[Config], annotations: Ls[Annot])(using State) =
val tSym = TermSymbol(syntax.Fun, owner, Tree.Ident(sym.nme), erasedType = N)
// * Generated callables have a known function representation even when their result is unknown.
// * In particular, lowering a lambda must not introduce a checked Function cast that makes
// * its uses opaque to dead-parameter elimination and deforestation.
// * Definitions without parameter lists are getters, whose value representation is still unknown.
val erasedType = Option.when(params.nonEmpty):
ErasedType.FuncRef(S(false), params.map(_.params.map(_.sym.erasedType)), N)
val tSym = TermSymbol(syntax.Fun, owner, Tree.Ident(sym.nme), erasedType)
sym.tsym = S(tSym)
FunDefn(owner, sym, tSym, params, body)(configOverride, annotations)

Expand Down Expand Up @@ -1159,6 +1166,10 @@ sealed abstract class Result extends Located, HasErasedType:
case Value.Lit(_: Tree.StrLit) => S(ErasedType.Str)
case Value.Lit(_: Tree.BoolLit) => S(ErasedType.Bool)
// * Note: `UnitLit` stays untyped: Neither `null` nor `undefined` can be reasonably typed as `Unit`
// * WORKAROUND (see `semantics.BuiltinOperatorResults`): builtin operators have no declared signature,
// * so their results are approximated from the representations of their operands.
case Call(Value.SimpleRef(op: BuiltinSymbol), args :: Nil) if args.forall(_.spread.isEmpty) =>
ErasedType.builtinOperatorResult(op.nme, args.map(_.value))
case Call(fun, argss) => fun.targetSymbol match
case S(ts: TermSymbol) => ts.erasedType match
case S(ErasedType.FuncRef(rsc, paramLists, ret)) =>
Expand Down Expand Up @@ -1190,8 +1201,21 @@ sealed abstract class Result extends Located, HasErasedType:
case sym => sym.asCls.flatMap(_.erasedType)
// * A tuple literal is typed as `Array` at runtime.
case Tuple(_, _) => S(ErasedType.Array)
// * Avoid a redundant cast around a function literal: in JavaScript that
// * would also prevent assignment from supplying the function's inferred name.
case _: Lambda => S(ErasedType.Function(S(false)))
case _ => N

/** `undefined` is an unspecified value of any representation, including unboxed primitives.
* Casts retain the expected representation but do not constrain the underlying unspecified value.
* Reading back an `undefined` stored in a slot is undefined behavior (see Runtime Representations in
* `doc/reference.md`), so a backend may materialize it as any value of the slot's representation.
*/
def isUndefined: Bool = this match
case Value.Lit(Tree.UnitLit(false)) => true
case Cast(value, _, _) => value.isUndefined
case _ => false

/** Coerces this result to `expected`, yielding it unchanged when no coercion is required.
*
* Narrowing to an unrelated type is reported as an error, and this result is yielded unchanged.
Expand All @@ -1201,26 +1225,39 @@ sealed abstract class Result extends Located, HasErasedType:
* [[Config]] of their own.
*/
def coerceTo(expected: ErasedType, loc: Opt[Loc])(using Ctx, State, Raise, Config): this.type | Cast =
coerceToOr[this.type | Cast](expected, loc)(identity): (actual, declared) =>
raise:
ErrorReport(msg"Cannot use a value of type '${actual.describe}' at an unrelated type '${declared.describe}'" -> loc :: Nil,
source = Diagnostic.Source.Compilation)
this

// `coerceTo` continuing with `coerced`, except that a value of a type unrelated to `expected` goes to `unrelated`
def coerceToOr[R](expected: ErasedType, loc: Opt[Loc])(coerced: (this.type | Cast) => R)
(unrelated: (CanonicalErasedType, CanonicalErasedType) => R)(using Ctx, State, Raise, Config): R =
val actual = erasedValueType_!.canonicalize
val declared = expected.canonicalize
ErasedType.needsCast(actual, declared) match
case S(false) => this
val cast =
if isUndefined && !declared.isInstanceOf[ErasedType.Incompatible] then S(true)
else ErasedType.needsCast(actual, declared)
cast match
case S(false) => coerced(this)
case S(true) =>
val target = expected match
case ft: ErasedFuncType => ErasedType.Function(ft.rsc)
case v: ErasedValueType => v
Cast(this, target, config.checkCasts)(loc)
coerced(Cast(this, target, config.checkCasts && !isUndefined)(loc))
case N =>
// * An `Incompatible` side is not an unrelated type but an unrepresentable one, so it gets its own message.
def membersOf(et: CanonicalErasedType): Opt[(CanonicalErasedValueType, CanonicalErasedValueType)] = et match
case ErasedType.Incompatible(l, r) => S(l -> r)
case _ => N
val message = membersOf(actual).orElse(membersOf(declared)) match
case S((l, r)) => msg"Types '${l.describe}' and '${r.describe}' have no common representation"
case N => msg"Cannot use a value of type '${actual.describe}' at an unrelated type '${declared.describe}'"
raise:
ErrorReport(message -> loc :: Nil, source = Diagnostic.Source.Compilation)
this
membersOf(actual).orElse(membersOf(declared)) match
case S((l, r)) =>
raise:
ErrorReport(msg"Types '${l.describe}' and '${r.describe}' have no common representation" -> loc :: Nil,
source = Diagnostic.Source.Compilation)
coerced(this)
case N => unrelated(actual, declared)

/* mayRaiseEffects indicates whether this call may raise effect (algebraic effect),
* regardless of whether the check for effect is inserted or not.
Expand Down Expand Up @@ -1335,15 +1372,17 @@ case class Instantiate(mut: Bool, cls: Path, argss: Ls[Ls[Arg]])(val metadata: I
*
* Invariants:
* - `value` is not a `Cast`.
* - `target` must be a proper subtype of `value`'s erased type.
* - `target` must be a proper subtype of `value`'s erased type, unless `value` is `undefined`, whose
* representation is supplied by the cast.
*/
case class Cast private(value: Result, target: ErasedValueType, check: Bool)(val toLoc: Opt[Loc]) extends Path:
def withLoc(loc: Opt[Loc]): Cast = if loc == toLoc then this else copy()(loc)

object Cast:
/** Builds a cast while collapsing a nested cast.
*
* This node is malformed if the target type is not a proper subtype of the value's erased type.
* Except for `undefined`, this node is malformed if the target type is not a proper subtype of the value's
* erased type.
*
* Collapsing `Cast(Cast(v, T), U)` to `Cast(v, U)` drops the inner test. The `T`-typed intermediate goes with it,
* so no value is left in a wrongly-typed slot. However, an unchecked failure *can be lost* - if a cast is
Expand Down
Loading