Type-checking a specification

Type-checking determines whether a specification is well-formed mathematically, independently of the actual networks, datasets and parameters it will be used with.

The standard type system includes checks that:

  • operations are applied to the right types of data (e.g. we do not add a Vector to a Bool).

  • variables are used consistently (e.g. the same variable x isn’t used as an Nat in one place and as a Tensor in another).

  • there are no out-of-bounds errors when indexing into Vector and Tensor (e.g. if xs is a vector of size 2 then we don’t index into it at any position other than 0 and 1).

Note that most other Vehicle commands will type-check the specification with the standard type-system automatically as part of their operation.

While 99% of the time the Standard type system is what you want, Vehicle also supports other type-systems as part of its internal operation:

  • Standard

  • Linearity (see this paper for details)

  • Polarity (see this paper for details)

  • Decidability

Command-line interface

A specification can be type-checked on the command-line using the vehicle typecheck mode.

vehicle typecheck \
  --specification my/project/specification.vcl

The table below contains the full list of possible arguments:

--specification, -s

The .vcl file containing the specification.

--typeSystem, -t

Optional. The type-system to use when checking the specification.

Python interface

A specification can be type-checked via the Python interface using the vehicle_lang.typecheck module:

vehicle_lang.typecheck.typecheck(specification: str | Path) → VehicleUserError | None

Type-check a .vcl specification file.

Parameters:

specification (str | Path) – The path to the Vehicle specification file to verify.

Returns:

None if type-checking succeeded, or a VehicleUserError if type-checking failed with a user error.

Raises:

VehicleInternalError – If the Vehicle command fails to execute.

Return type:

VehicleUserError | None