How to call host code from Lean

This guide shows how Lean code calls a function of the application, in the language of the generated package. For Rust, see how to call Rust functions from Lean; for operations the application answers asynchronously, see how to call async host operations.

Declare a facility in Lean

What the host provides is a facility: a declaration registered with @[lungo_facility], whose operations are @[extern] declarations marked @[lungo_operation]. The project requires lungo’s Lean library for the attributes.

import Lungo

namespace Store

/-- The application's store. -/
@[lungo_facility "store.data"]
structure Data

/-- The application's log. -/
@[lungo_facility "store.journal"]
structure Journal

/-- Looks a key up in the application's store. -/
@[extern "store_lookup", lungo_operation Data]
opaque lookup (key : @& String) : Option Nat

/-- Appends a line to the application's log. -/
@[extern "store_log", lungo_operation Journal]
opaque log (line : String) : IO Unit

def total (keys : List String) : IO Nat := do
  let mut sum := 0
  for k in keys do
    match lookup k with
    | some v => log s!"{k} = {v}"; sum := sum + v
    | none => throw (IO.userError s!"unknown key {k}")
  return sum

end Store

The facility’s identifier (store.data) names it in every package, and its last segment names it in each language (Data, set_data, data). An extern that is no facility’s operation and that neither the runtime nor the program implements is an error (LNG0401); an operation that the runtime or a Lean @[export] already implements is one too (LNG0706).

What Lean cannot check about the host, it can assume: an @[lungo_assumption Data] proposition says what the host’s implementation must satisfy, and claims that rest on it say so in every package (see how to declare facilities and assumptions).

Implement it

The generated package has, per facility, an interface (or protocol) with one method per operation, named after the Lean declaration and with its types, and an installer. An IO operation fails with the language’s IO error (any other error becomes IO.userError with its message); an operation that is not IO or EIO must not fail: its failure terminates the program. An operation whose Lean type is pure must also behave as a pure function, answering the same arguments the same way: Lean may compute lookup "a" once and keep the value.

Install every facility before the program’s first call. A call before then fails, naming the facility and one of its operations: Go returns a *lungo.MissingFacilityError, Python raises lungo_py.MissingFacilityError, Swift throws LungoMissingFacility, TypeScript’s load rejects with MissingFacilityError, and a C program ends with a message.

Go

type data struct{ values map[string]*big.Int }

func (d *data) Lookup(key string) (lungo.Option[*big.Int], error) {
	v, ok := d.values[key]
	return lungo.Option[*big.Int]{Value: v, Valid: ok}, nil
}

type journal struct{}

func (journal) Log(line string) error {
	log.Println(line)
	return nil
}

store.SetData(&data{values: map[string]*big.Int{"a": big.NewInt(1)}})
store.SetJournal(journal{})

Python

class Data:
    def lookup(self, key: str):
        return {"a": 1}.get(key)

class Journal:
    def log(self, line: str) -> None:
        print(line)

store.set_data(Data())
store.set_journal(Journal())

Swift

final class Table: StoreData {
    func lookup(_ key: String) throws -> LungoNat? { key == "a" ? 1 : nil }
}

final class Console: StoreJournal {
    func log(_ line: String) throws { print(line) }
}

setData(Table())
setJournal(Console())

TypeScript

const p = await load({
  facilities: {
    data: { lookup: (key) => (key === "a" ? 1n : null) },
    journal: { log: (line) => console.log(line) },
  },
});

C

static int32_t lookup(void *ctx, const lungo_value *const *args, size_t n, lungo_value **result, lungo_error **error) {
    size_t len;
    const char *key = lungo_value_get_string(args[0], &len);
    *result = len == 1 && key[0] == 'a' ? lungo_value_some(lungo_value_nat(1)) : lungo_value_none();
    return LUNGO_OK;
}

static int32_t log_line(void *ctx, const lungo_value *const *args, size_t n, lungo_value **result, lungo_error **error) {
    size_t len;
    const char *line = lungo_value_get_string(args[0], &len);
    printf("%.*s\n", (int)len, line);
    *result = lungo_value_unit();
    return LUNGO_OK;
}

store_implement_data_lookup(lookup, NULL, NULL);
store_implement_journal_log(log_line, NULL, NULL);

See what the program needs

lungo assurance lists, for every export, the facilities it needs and the assumptions its claims make of them; each package carries the same in its assurance document (see the assurance document).

Pass functions both ways

A Lean parameter of function type accepts a function of the host language, which Lean may call any number of times, on any thread, while it holds it; a Lean function returned to the host is a function the host calls. Both cross as described in the wire format; nothing needs declaring.