Using scryer-prolog as a Rust crate library

[segeljakt]

Hi, I am wondering if it's would be possible to use scryer-prolog as a library for Rust applications.

I am asking because I'd be really interested to use it for the type inference component of a programming language I'm working on (also implemented in Rust).

[ghost]

The idea of using Scryer as a library has been requested some times (#225, #570).

It should be possible. Do you have a template in Prolog?

[segeljakt]

Woops, sorry I should have checked the previous issues closer.

I have two examples which I have written in the Datalog subset of Prolog using crepe:

1. Type inference for a calculus with primitive types.

For example, infer the type of each expression in the term:

let x = 50i32 + 100i32 in x == 150i32

Also, detect if there are any un-typeable terms, e.g. in:

let x = 50i32 + 100i32 in x == 150u32

2. Ownership-checking for a calculus with tuples and projection:

For example, check whether there are any ownership violations in:

let a = (("foo", 5), "bar") in
let b = a.0.0 in
let c = a.0.1 in
let d = a.1 in
1
// Expected result: OK

Another example:

let a = (("foo", 5), "bar") in
let b = a.0.0 in
let c = a.0.1 in
let d = a.0 in
1
// Expected result: Use of moved value `a.0`.

Datalog is great but also limited in what it can express. I'm interested in extending the type inference example with parametric polymorphism, and eventually ad-hoc polymorphism. For now, I think a good starting point might be to try re-implement the type-inference example's crepe code as scryer-prolog library calls.

To check if the two sides of an addition are equal, the facts currently look like:

// typeof(a + b)
TypeOf(e0, tk0) <-
    ExprOf(e0, ek0),
    let ExprKind::Add(e1, e2) = ek0,
    TypeOf(e1, tk0),
    TypeOf(e2, tk0);

// typeof(100i32)
TypeOf(e0, TypeKind::I32) <-
    ExprOf(e0, ek0),
    let ExprKind::I32(_) = ek0;

How would something equivalent look in the scryer-prolog API?

[ghost]

The Addition is a function, you can generalize it. An example in Prolog:

Here

:- use_module(library(debug)).
:- use_module(library(freeze)).
:- use_module(library(lists)).
:- use_module(library(pairs)).

i32(N, i32) :- integer(N).
u32(N, u32) :- integer(N), N >= 0.
bool(true, bool).
bool(false, bool).

% name, arguments, return
fn(foo, [bool, bool, bool], bool).
fn(foo, [u32, i32], bool).

program([let(a, _, 1), let(b, _, 1), let(c, _, foo(a, b))]).

let_pair(let(N, T, _), N-T).

ty_infer(KVs) :-
    program(P),
    maplist(let_pair, P, KVs),
    ty_infer_(P, KVs).

ty_infer_([], _).
ty_infer_([L|Ls], KVs) :-
    let(_, T, V) = L,
    get_type(KVs, V, T),
    ty_infer_(Ls, KVs).

get_type(KVs, V, T) :-
    nonvar(V),
    (   V =.. [Id|Args],
        fn(Id, Ts, T),
        pairs_keys_values(Ps, Args, Ts),
        maplist(set_type(KVs), Ps) ->
        true
    ;   freeze(
            T,
            (   bool(V, T) ->
                true
            ;   i32(V, T) ->
                true
            ;   u32(V, T)
            )
        )
    ).

set_type(KVs, KV) :-
    (   member(KV, KVs) ->
        true
    ;   throw(error(unknown_variable(KV)))
    ).

To run the test:

$ scryer-prolog test.pl
?- ty_infer(Vs).
   Vs = [a-u32,b-i32,c-bool].
?-

The result can be retrieve with system predicate or it could be printed.

[segeljakt]

Ok, this looks promising. Is there some way to pass input/output to the program from/to Rust?

[ghost]

The system predicate is the easiest way to pass input/output. There is also Stream in Rust but there are fewer lines on how to use, what is possible.

[segeljakt]

I see, what I'm looking for is more of an FFI. As I understand, this is not possible?

[ghost]

There isn't any FFI, it could be useful if some C codes or any others want to interact with or integrate Scryer. If it is a Rust only project then there isn't a need for one yet else you will have to implement all of it (create a machine, pass data, retrieve data, ...).

[XVilka]

A heads up for anyone subscribed to this issue - the initial work is here https://github.com/mthom/scryer-prolog/pull/838

[Skgland]

the work in #2465 might also help the usability from rust even though its primary aim is to facilitate usage as a dynamic library