Type checking a specification

Type-checking determines whether a specification makes sense mathematically, independent of what networks, datasets and parameters it will be used with.

This includes:

• that operations are applied to the right types of data (e.g. that it doesn’t add a Vector to a Bool).

• that 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).

• that 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 use index into it at any position other than 0 and 1).

Note most other Vehicle commands will type-check the specification automatically.

Command-line interface

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

vehicle check \
  --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

The type-system to use when checking the specification. 90% of the time you should not provide any value for this option as the default value Standard is what you want. However there are two further options Linearity and Polarity which means are used by Vehicle to diagnose errors with how quantified variables are used (see this paper for details).