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 aBool
). - that variables are used consistently (e.g. the same variable
x
isn't used as anNat
in one place and as aTensor
in another). - that there are no out-of-bounds errors when indexing into
Vector
andTensor
s (e.g. Ifxs
is a vector of size 2 then we don't use index into it at any position other than0
and1
).
- that operations are applied to the right types of data (e.g. that it doesn't add a
Note most other Vehicle commands will type-check the specification automatically.
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).