Implicit parameters are always integers, and they must appear first before any other parameters in the function type signature. This signature shows how Sail can track the length of bitvectors and the value of integer variables in type signatures, using type variables. First we can write the type signature for the function using the val keyword, then define the body of the function using the function keyword. Type constructors therefore have types much like functions, with list having the type Type → Type and range having the type (Int, Int) → Type . Match can also be used to destructure tagged union constructors, for example using the option type from the Sail library.