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 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
(e.g. ifxs
is a vector of size 2 then we don’t use index into it at any position other than0
and1
).
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 optionsLinearity
andPolarity
which means are used by Vehicle to diagnose errors with how quantified variables are used (see this paper for details).