_`?→_†

Definitions:

any, type
Source: /avail/Avail/Foundation/Casts
Categories: Casts
Cast the value into the specified statically evaluated type. If the value at runtime does not comply with this type, fail the same way any call overly strengthened by a semantic restriction would fail.
Position Name Type Description
Parameters
1 value any The value whose type is to be strengthened.
2 strongerType type Evaluated at compile time to produce the strengthened type of this call.
Returns any Restricted to the strongerType.

Semantic restrictions:

valueType, strongerMeta, elseFunctionType
Source: /avail/Avail/Foundation/Casts
Cast the value into the specified statically evaluated type. If the value at runtime does not comply with this type, return instead the result of evaluating the zero-argument elseFunction.

The value's static type and the provided type must have a non-⊥ intersection. Additionally, the value's static type must not already be sufficiently strong by being a subtype of the provided type. The resulting type of the call site is the union of the else function's return type and the intersection of the value's static type and the provided strengthening type. Note that this means it is acceptable for the else function to produce a value that is not in compliance with the specified strengthening type. This has value when the goal is to type check, strengthen, and alternatively run arbitrary code for side-effect and return an otherwise out-of-band sentinel, which was specifically excluded in the type check.

Type Description
Parameter Types
valueType any's type The static type of the expression whose type is to be strengthened.
strongerMeta type's type Evaluated at compile time to produce the strengthened type of this call. The actual type is passed at runtime, but the metatype is what gets provided to this semantic restriction.
elseFunctionType ([]→any)'s type What to do in case the value being tested does not comply with the strengthening type. The result of running this function will be used as the call site's resulting value.
valueType, strongerMeta
Source: /avail/Avail/Foundation/Casts
Cast the value into the specified statically evaluated type. If the value at runtime does not comply with this type, fail the same way any call overly strengthened by a semantic restriction would fail.

The value's static type and the provided type must have a non-⊥ intersection. Additionally, the value's static type must not already be sufficiently strong by being a subtype of the provided type. The resulting type of the call site is the intersection of the value's static type and the provided type.

Type Description
Parameter Types
valueType any's type The static type of the expression whose type is to be strengthened.
strongerMeta type's type Evaluated at compile time to produce the strengthened type of this call. The actual type is passed at runtime, but the metatype is what gets provided to this semantic restriction.