Backends

An instance of HasBackend, that implements the main connection to the pipeline:

• The datatype used for types, values and errors (Ty, Val, Err

respectively);

• stdlib, the Juvix source file(s) that make up the standard library for

this backend;

• Optionally an implementation for the parse function;

• Optionally an implementation for the typecheck function;

• An implementation for the compile function.

We need to inform the Juvix compiler of some basic information about our backend, such as:

• A function for typechecking primitives: hasType.

• Lists of builtin values and types: builtinTypes and builtinValues.

• Functions for creating primitives based on a literal integers, floats or strings: stringVal, intVal and floatVal.

For compilation, the backend takes a representation of the input program that is very close to a primitive-extended lambda calculus with multi-argument lambda's. As the primitives of the target language themselves can be functions, for example basic arithmetic operators, we can normalize these terms as well. For this we need to instantiate two classes for the primitives:

• HasSubstV: For substitution of term.

• HasWeak: For weakening of terms (accounting for removal of a lambda abstraction).

• HasPatSubstTerm: Substitution of patterns.

Each of these are documented in more detail at the evaluator page.

Additionally, to make applying terms possible during substitution, the CanApply class needs to be instantiated for primitive terms and types.