Witness-indexed types

Most extension questions are resolved at the call that needs a capability. A witness-indexed type is useful when the choice must remain the same for the whole lifetime of a value. Its witness argument becomes part of the value’s static type, while the represented value keeps its ordinary layout.

The standard library’s SortedMap is the motivating example: every lookup, update, and iteration must use the ordering selected when the map was created. See Sorted maps for the user-facing collection API.

Declare a witness parameter

A nominal type puts its witness parameters after its ordinary type parameters:

export datatype SortedMap[
  K,
  V,
  extension Key: IOrderedKey for K,
]
  SortedMap{tree: Tree[K, V]}
end

Key is a static parameter. It is not a field in SortedMap, and it does not add a constructor argument that user code has to pass manually. The goal says which interface the witness must implement and which type it describes.

Use an indexed type

All trailing witness arguments may be omitted when ordinary inference or extension resolution can determine them:

func main() -> Unit do
  numbers : SortedMap[Int, String] = SortedMap.empty();
  numbers = numbers.set(2, "two");
  numbers = numbers.set(1, "one");
  Debug.trace(numbers.get(1));
end

SortedMap[Int, String] is shorthand for a complete type application with a concrete IOrderedKey for Int witness. The omitted witness is inferred; it is not an existential type and it is not a request to forget the ordering choice. When no unique witness can be found, the declaration or call is rejected.

To make the witness relationship explicit, write it in the type application:

func empty_with_order[K, V](
  ?{extension Key: IOrderedKey for K},
) -> SortedMap[K, V, extension Key] do
  SortedMap.empty(?{Key: Key})
end

The question binds Key, and the result type records that same witness. The constructor receives the selected witness through the ordinary contextual question mechanism, so constructors and helper functions use one consistent resolution path.

Extract a witness from an indexed value

A function parameter can bind the witness already carried by a static type. Use |extension Name| in the type-pattern position, then refer to that witness as extension Name in later types or as Name in the function body:

func find[K, V](
  map : SortedMap[K, V, |extension Key|],
  key : K,
) -> Option[V] do
  map.get(key)
end

func same_order[K, V](
  _left : SortedMap[K, V, |extension Key|],
  right : SortedMap[K, V, extension Key],
) -> SortedMap[K, V, extension Key] do
  right
end

The repeated extension Key requires identity equality, not merely two providers that happen to implement the same interface. This lets APIs preserve the relationship between several indexed values without storing a dictionary inside each value.

Witness identity is part of type equality

Two providers can satisfy the same goal and still produce different indexed types. The following applications are intentionally incompatible:

SortedMap[Int, String, extension Ordering.Ascending]
SortedMap[Int, String, extension Ordering.Descending]

There is no implicit conversion that drops or replaces a witness index. This prevents a later call from silently using a different ordering than the one chosen at construction. If an API really needs to hide that choice, it needs an explicit erasure design; version 1 does not provide existential witness erasure.

No runtime wrapper

Witness indices describe static relationships only. A value such as

SortedMap::SortedMap{tree: tree}

has the same runtime representation for every ordering witness. The compiler passes a dictionary through a private question slot when generic code binds a witness, rather than reading a Key field from the map. This keeps the abstraction zero-cost in the value layout while preserving type-safe dispatch.

Rules to remember

• Ordinary type parameters must come before witness parameters.
• Witness parameters are trailing, and partial positional omission is not allowed: either provide all witness arguments or let all of them be inferred.
• An omitted witness must be fixed by an indexed input, an existing contextual witness, a named provider, or unique extension resolution before the declaration is finalized.
• A return type cannot invent an unconstrained witness. Introduce one with a contextual question or bind it from an indexed parameter.

Witness-indexed types build on question parameters and interfaces and extensions. For a complete example of the resulting collection behavior, continue with Sorted maps.

Next: Operator overloading.