wikifn-fstar

Wikifunctions as SPARQL extension functions

A SPARQL 1.1 engine (Comunica, loaded from a CDN) querying a small local dataset, where the functions in the FILTER and BIND clauses are real Wikifunctions. Both engines run in this page. Nothing is sent anywhere.

The Wikifunctions side is the F*-extracted engine: translated from the pinned corpus into F*, checked by F*, extracted to OCaml, compiled to JavaScript. Every function it can run is available here, addressed by ZID.

A SPARQL extension function here is a compiled F* function, not a tree walk. Each of 1,370 compositions is an F* definition that F* checks and that extracts to an OCaml function and then a JavaScript one, so fn:Z10096(...) in a query below is a function call. Where a ZID has no compiled function the page falls back to the interpreter and says so in the result, rather than quietly answering from a different path.

Engine browser · What still fails · How it works

Why canals

A canal is a passage you can transit in either direction and arrive at the same canal. A palindrome is a string you can read in either direction and arrive at the same string. The Panama Canal is the one place where those two facts meet, because of Leigh Mercer's A man, a plan, a canal: Panama — which is a palindrome only once you throw away the spaces and punctuation.

So the dataset below is waterways, each with a phrase, and the query asks which phrases are palindromes after their spaces are removed. That is two Wikifunctions composed inside a FILTER: Z10052 remove regular spaces, then Z10096 is a palindrome. Neither was written here; both come from the corpus with a revision and a digest.

Run it

Starting…

How the binding works

Comunica takes an extensionFunctionCreator: given the IRI of an unknown function, return something callable or undefined. That is the whole integration, and it is why every ZID works rather than a chosen few.

const engine = new Comunica.QueryEngine();

await engine.queryBindings(query, {
  sources: [{ type: "serialized", value: turtle, mediaType: "text/turtle" }],

  // Any <.../fn#Znnnn> becomes a call to the compiled F* function for it.
  extensionFunctionCreator: (iri) => {
    const zid = /#(Z[1-9][0-9]*)$/.exec(iri.value)?.[1];
    if (!zid) return undefined;
    return (args) => toTerm(JSON.parse(globalThis.wikifnCompiledCall(
      zid, JSON.stringify(args.map(fromTerm)))));
  }
});

The two conversions are the only real work: SPARQL passes RDF terms and the engine takes JSON literals, so a xsd:string becomes a string, an xsd:integer a natural number, xsd:boolean a boolean, and the result envelope (Z6 text, Z40 boolean, Z13518 natural number) converts back. Anything else is refused rather than guessed at.

What this is and is not

The Wikifunctions side is the same artifact the engine browser runs, checked by F* and measured against Wikifunctions' own testers. The SPARQL side is stock Comunica; nothing about it is modified.
Compiled and interpreted must give the same answer, and a test requires it on every argument the corpus's own testers supply. The compiled path is not a faster approximation of the other one.
A function that is not runnable, or that reaches a group of compositions defined through each other with no base case, will report that rather than return a value. The error surfaces as a SPARQL error, not as a wrong answer.
Only strings, natural numbers and booleans cross the boundary today. Lists and records exist in the engine but have no obvious RDF term, so they are refused.
This is a demonstration that the extraction is usable from an unrelated host, not a proposal for how Wikidata should call Wikifunctions.

The dataset

Six waterways and a phrase each, as Turtle. Editable is not the point; it is here so the query is readable.