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:

class vehicle_lang.typecheck.TypeSystem(value)

The type systems supported by Vehicle.

vehicle_lang.typecheck.typecheck(specification: str | Path, *, typeSystem: TypeSystem = TypeSystem.Standard) → str

Type-check a .vcl specification file.

Parameters:

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

  • typeSystem (TypeSystem) – The type system that should be used.