Foreign Functions

Foreign functions allows for complex value manipulation in Scallop. Conceptually, they are pure and partial functions that operate on value(s) and return one single value only. Functions with states, such as random, are not allowed as foreign functions.

Function Types

In Scallop, foreign functions are generically typed with optional and variable arguments. All the functions have a dollar sign ($) associated with the function name. We use the following syntax to denote a function signature

$FUNC_NAME<ARG(: FAMILY)?, ...>(
  POS_ARG: POS_ARG_TYPE, ...,
  OPT_ARG: OPT_ARG_TYPE?, ...,
  VAR_ARG_TYPE...
) -> RETURN_TYPE

The generic arguments are specified in the <...> after the function name, and can be annotated by optional type family. For the arguments of the function, optional arguments have to appear after all positional arguments, and the variable arg type must appear after all positional and optional arguments. Functions must have a return type.

For example, the function $string_char_at(s: String, i: usize) -> char takes in a string s and an index i, and returns the character at that location. The two arguments s and i are both positional arguments.

In the function $substring(s: String, b: usize, e: usize?), we have 2 positional arguments (s and b) and 1 optional argument (e). This means that this substring function can be invoked with 2 or 3 arguments. Invoking $substring("hello", 3) would give us "lo", and invoking $substring("hello", 1, 3) would give us "el".

For functions like $abs<T: Number>(T) -> T, we have absolute value function taking in value of any type that is a number (including integers and floating points). The function also returns a type the same as the input.

For a function like $format(f: String, Any...), it looks at the format string and fill all the {} symbol in the string with the latter arguments. Notice how there can be arbitrary number of arguments (variable arg) of Any type. For example, we can have $format("{} + {}", 3, "a") ==> "3 + a" and $format("{}", true) ==> "true".

Function Failures

Foreign functions may fail with errors such as divide-by-zero, index-out-of-bounds. When error happens, values will not be propagated along the computation, and will be dropped silently.

For example, the following program makes use of the foreign function $string_char_at. It walks through the indices 1, 3, and 5, and get the character on those indices of the string "hello".

rel indices = {1, 3, 5}
rel output(i, $string_char_at("hello", i)) = indices(i)

However, there are only 5 characters in the string, meaning that getting the 5-th character would result in an index-out-of-bounds error. Scallop will drop this invokation silently, resulting in only two facts being derived:

output: {(1, 'e'), (3, 'l')}

Similar things happen when nan is derived from floating point operations, or that the foreign function fails.

Library of Foreign Functions

We hereby list all the available foreign functions, their signatures, descriptions, and an example of how to invoke them. The functions here are ordered alphabetically. For some of the functions that are slightly more complicated (e.g. $format), please refer to the section below for more information.