Function encoding¶

Functions are encoded as the pair of a natural number identifier (specifying a particular virtual machine) and bytecode (to be interpreted by the virtual machine):

type Function := mkFunction {
    vmIdentifier : Natural;
    vmBytecode : []byte;
};

We then define the canonical function encoding functions as a switch-case over these particular virtual machines.