Advanced topics (TODO)

This page contains advanced topics about the specification language. These shouldn’t be necessary to read in order to get going with Vehicle but may be of interest to advanced users.

Dependent functions

Unlike many common strongly-typed languages, Vehicle is dependently typed and so if you have a function type A -> B, the type B may depend on the value passed for A. For example (n : Nat) -> Tensor Rat [n] is the type of a function that takes in a natural number n and returns a vector of rationals of length n.