Programming Language Semantics in Prolog

It's mostly here to compare and contrast with similar work for the Joy language:

A simple language

We're going to talk about a language based on the one in Hamel's paper, which is "a small functional language inspired by Winskel’s REC language."

letrec(f, y, 
    if(variable(y), 
        apply(
            variable(f),
            add(variable(y), mu(number(1)))
            ),
        add(variable(y), number(1))
        ),
    apply(variable(f), number(7))
    ).

It's not a very useful language *per se*, it has only integers and closures, no loops (you must use recursive functions), and no fancy scoping rules. What it is good for is exploring the meta-linguistic aspects of programming languages.

The first thing we need is a way to convert text data into Abstract Syntax Trees describing the structure of the code. We lex the characters into tokens and then parse the tokens into AST. From the AST we can evaluate the code, deduce the type signature of it, compile it to some other form (i.e. C or assembly or whatever), and so on.

Lexer

Information about the language operators is kept in a couple of "tables". We have a single prefix operator (I call it "mu" for no reason) to negate integers and two binary infix operators for addition and multiplication. As you saw in the example code above to subtract you must add a negative number.

prefix_op(mu, "-", Bar, mu(Bar)).

infix_op(add, "+", 750, Left, Right, add(Left, Right)).
infix_op(mul, "*", 500, Left, Right, mul(Left, Right)).

keyword(arrow, "→").
keyword(assign, "≔").
keyword(else, "else").
keyword(end, "end").
keyword(fn, "λ").
keyword(if, "if").
keyword(in, "in").
keyword(let, "let").
keyword(rec, "rec").
keyword(then, "then").

Lex a list of lexemes.

Turning a list of character codes into a list of lexemes is pretty straightforward.

lex([Lexeme|Rest]) --> lexeme(Lexeme), !, lex(Rest).
lex(        Rest ) --> blanks,         !, lex(Rest).
lex([])            --> [].

lexeme('(') --> "(".
lexeme(')') --> ")".

lexeme(operator(Name)) -->
    { infix_op(Name, Op, _, _, _, _)
    ; prefix_op(Name, Op, _, _) },
    Op.

Keywords are slightly tricky only because they must be followed by blanks or nothing (because ``end`` keyword ends the character list without trailing blanks) to prevent matching prefix of identifiers.

lexeme(KW) -->
    { keyword(KW, Codes) },
    Codes,
    (blanks | end).

Identifiers mustn't be keywords. Integers follow the usual rules for decimal notation.

lexeme(ident(ID)) -->
    identifier(Codes),
    { atom_codes(ID, Codes),
      \+ keyword(ID, _) }.

lexeme(number(N)) -->
    number(Codes),
    { number_codes(N, Codes) }.

Character Pattern Recognizers.

identifier([Ch|Rest]) -->
    (alpha(Ch) | underscore(Ch)),
    z(Rest, ident_char).

number([InitialDigit|Digits]) -->
    digit(InitialDigit),
    z(Digits, digit).

digit(Ch) --> [Ch], { nonvar(Ch),
                      between(0'0, 0'9, Ch) }.

alpha(Ch) --> [Ch], { nonvar(Ch),
                    ( between(0'a, 0'z, Ch)
                    | between(0'A, 0'Z, Ch)
                    ) }.

underscore(0'_) --> "_".

ident_char(Ch)  --> alpha(Ch) | underscore(Ch) | digit(Ch).

blanks --> " ", blanks | " ".

end([], []).  % Match end of list.

% Greedy zero_or_more meta-DCG.
z([Term|List], F) --> call(F, Term), !, z(List, F).
z([],          _) --> [].

Table-driven Operator Precedence Expression Parser

expression(Expr) -->
    { max_prio(MP) },
    expression(MP, Expr).

expression(Priority, Expr) -->
    primary(LHS),
    rest_expression(LHS, 0, Priority, Expr).

rest_expression(LHS, CurPriority, MaxPriority, Expr) -->
    operator(CurPriority, MaxPriority, LHS, RHS, Out, OpPriority),
    !,
    % ops of higher precedence
    expression(OpPriority, RHS),
    % ops of lower precedence
    rest_expression(Out, OpPriority, MaxPriority, Expr).

rest_expression(Expr, _, _, Expr) --> [].

% Look-ahead one Token.
primary(Primary) --> [Token], primary(Token, Primary).

primary(    ident(X), variable(V)) --> rest_var(X, V).
primary(   number(X),   number(X)) --> [].
primary(         '(',        Expr) --> expr(Expr), [')'].  % N.B.: expr//1 not expression//1.
primary(operator(Op),        Expr) --> { prefix_op(Op, _, Arg, Expr) }, primary(Arg).

operator(CurPriority, MaxPriority, LHS, RHS, Out, OpPriority) -->
    [operator(Op)],
    { infix_op(Op, _, OpPriority, LHS, RHS, Out),
      OpPriority >= CurPriority,
      OpPriority  < MaxPriority }.

(What is that ``rest_var//2``? I don't know. It's part of O'Keefe's parser code, a hook for the user/client, but to what end? I dunno. i just unify the ``X`` and ``V`` so that variables have the name of their identifiers.)

max_prio(1001).

rest_var(X, X) --> [].  % Look up X or something?

Grammar

expr(fn(Name, Expr)) -->
    [fn, ident(Name), arrow], expr(Expr).

expr(if(Test, Then, Else)) -->
    [if], expr(Test),
    [then], expr(Then),
    [else], expr(Else),
    [end].

expr(let(Name, Value,  Expr)) -->
    [let, ident(Name), assign], expr(Value),
    [in], expr(Expr),
    [end].

expr(letrec(F, Name, FnBody, Expr)) -->
    [let, rec, ident(F), ident(Name), arrow], expr(FnBody),
    [in], expr(Expr),
    [end].

expr(apply(Fn, Arg)) --> expr(Fn), expression(Arg).

expr(Expr) --> expression(Expr).

Parser

Because the expression precedence parser and the grammar are DCGs the parser is just ``phrase/2``, however to handle application as 'E = E E' we need iterative deepening...

parse(Source, AST) :- parse(Source, AST, _), !.

parse(Source, AST, Reached) :-
    phrase(lex(Tokens), Source),
    length(_, Limit),
    call_with_depth_limit(
        phrase(expr(AST), Tokens),
        Limit,
        Reached
    ),
    Reached \= depth_limit_exceeded.

It's a little weird in my opinion to let application be unmarked by any special symbol or keyword (or putting the args in parentheses) but this is traditional in functional programming languages. It allows for elegant currying syntax, e.g. notice how you just write ``add 1 1`` here:

As abstract syntax ``E := E E`` is fine, but when you want to make a machine do it you must deal with the implied recursion. In Prolog DCGs the standard technique is to break the left-recursive with an extra term, or you can just use iterative deepening like I do here. (I think I might have also done the other thing? ``expr//1`` vs ``expression//1``? Or did I get it backwards? TODO: figure this out and nail it down. heh.)

Abstract Syntax Tree

fn(Name, Expr)
if(Test, Then, Else)
let(Name, Value,  Expr)
letrec(F, Name, FnBody, Expr)
apply(Fn, Arg)

variable(V)
number(N)

mu(Bar)
add(Left, Right)
mul(Left, Right)

The first five are encoded in the grammar rules, variables and numbers are encoded in the expression parser, and the last three are encoded in the operator definitions.

If ... then ... else statements with zero as Boolean *false* and non-zero integers as Boolean *true*::

let(y, number(0),
    let(m, number(7), 
        if(
            add(number(23), variable(y)),
            variable(m),
            number(23)
        )
    )
)

Recursive functions can be used in their own expressions. (Note the addition of a negative number to subtract)::

Semantics

I'm not sure why there are separate contexts for recursive functions and variables (but maybe that's only because I used Python for so long.) I use assoc lists rather than plain ol' lists and a ``closure/3`` term for closures rather than ``[[...]]``, but other than that this is pretty much the same code. Hamel uses ``::`` and ``-->>`` but I just use ``meaning/4``. E.g. in Hamel's paper this:

(Functions, Variables) :: Expr -->> Value

meaning(Expr, Value, Functions, Variables)

(Although tradition might suggest meaning(Expr, Functions, Variables, Value) as a better arrangement, eh? Output vars last, yes?)

With all that out of the way we can establish the semantics of the language. This is pretty straightforward.

To start out we initialize the function and variable namespaces and pass into ``meaning/4``::

meaning(Expr, Value) :-
    empty_assoc(Functions),
    empty_assoc(Variables),
    meaning(Expr, Value, Functions, Variables).

meaning(number(N), N, _, _).

meaning(variable(Name), Value, Functions, Variables) :-
      get_assoc(Name, Variables, Value)
    ; get_assoc(Name, Functions, Value).

meaning(mul(A, B), Value, Fs, Vs) :-
    meaning(A, AValue, Fs, Vs),
    meaning(B, BValue, Fs, Vs),
    Value #= AValue * BValue.

meaning(add(A, B), Value, Fs, Vs) :-
    meaning(A, AValue, Fs, Vs),
    meaning(B, BValue, Fs, Vs),
    Value #= AValue + BValue.

meaning(mu(A), Value, Fs, Vs) :-
    meaning(A, AValue, Fs, Vs),
    Value #= 0 - AValue.

meaning(if(Test, Then, Else), Value, Fs, Vs) :-
    meaning(Test, Flag, Fs, Vs),
    if_tail(Flag, Then, Else, Value, Fs, Vs).

if_tail(Flag, Then, _, Value, Fs, Vs) :-
    Flag #\= 0,
    meaning(Then, Value, Fs, Vs).

if_tail(Flag, _, Else, Value, Fs, Vs) :-
    Flag #=  0,
    meaning(Else, Value, Fs, Vs).

(I don't know for sure that it makes sense to use CLP(FD) constraints for the Boolean checks, but what the heck.)

The ``let`` expression assigns a value to a name in the variable binding environment::

meaning(let(Name, ValueExpr, S), Value, Fs, Vs0) :-
    meaning(ValueExpr, ValueValue, Fs, Vs0),
    put_assoc(Name, Vs0, ValueValue, Vs),
    meaning(S, Value, Fs, Vs).

The ``let rec`` expression assigns a function closure to a name in the function declaration environment. (Note the inclusion of the current variable binding environment in the closure)::

meaning(letrec(F, Name, FnBody, S), Value, Fs0, Vs) :-
    put_assoc(F, Fs0, closure(Name, FnBody, Vs), Fs),
    meaning(S, Value, Fs, Vs).

meaning(fn(Name, Body), closure(Name, Body, Vs), _, Vs).

Function applications look up a closure value in the function declaration or variable binding environments, get the argument value, bind it to the closure argument name in the variable binding environment, and then find the ``meaning/4`` of the body expression to get the value of the whole application::

meaning(apply(Fn, Arg), Value, Fs, Vs) :-
    meaning(Fn,   closure(Name, Body, FnVs0), Fs, Vs),
    meaning(Arg,  ArgValue,                   Fs, Vs),
    put_assoc(Name, FnVs0, ArgValue, FnVs),
    meaning(Body, Value,                      Fs, FnVs).

Evaluation

evaluate(Source, Value) :-
    parse(Source, AST),
    meaning(AST, Value).

Using ``evaluate/2``, source code on the left of the ``==>`` and value on the right:

Typing

Here we keep track of types in an environment (an assoc list, ``t`` is the empty assoc list.) In order to pass it along with less visual clutter I've written the typing predicate as a DCG. (Some Prolog systems insist that the underlying data structure is a list, but in SWI Prolog at least you can use an assoc list or whatever you want.)

Because I'm only using one environment for both functions and variables I don't think the typing code precisely mimics the semantic code, which is bad, but you're not supposed to use this language for anything anyway, so it doesn't really matter. The point is to show how you would do this stuff in general, not to make a set of rigorous tools for a toy language

typical(AST, Type) :- typical(AST, Type, t, _).

typical(number(_), int) --> [].

Variables are looked up in the type environment using ``close_over//1`` (so they had better be there, using ``let`` or ``let rec``, or typing will fail. We could just enter them here and let the actual type be determined later. This would allow it to "guess" the type of e.g. ``x * y`` by assuming that each variable is ``int`` typed.):

typical(variable(Name), Type) -->
    close_over(Env),
    { get_assoc(Name, Env, Type) }.

``close_over//1`` (as ``close_over/3`` but used as a DCG) grabs the current type assoc list environment::

close_over(E, E, E).

typical(mul(A, B), int) -->
    typical(A, int),
    typical(B, int).

typical(add(A, B), int) -->
    typical(A, int),
    typical(B, int).

typical(mu(A), int) --> typical(A, int).

If ... then ... else statements require an ``int`` for their test value and the ultimate type is the type of the branch.

Note that this creates a choice point in the Prolog control flow. Both branches' types are considered. This implies that an expression will have 2x types per branch, and would need some way to unify those types as some sort of "Either" type or we can insist that they are the same type, as we do here:

typical(if(Test, Then, Else), Type) -->
    typical(Test, int),
    ( typical(Then, Type)
    | typical(Else, Type)
    ).

typical(let(Name, ValueExpr, S), Type) -->
    typical(ValueExpr, ValueType),
    type_put(Name, ValueType),
    typical(S, Type).

typical(letrec(F, Name, FnBody, S), Type) -->
    close_over(Env),
    type_put(F, closure(Name, FnBody, Env)),
    typical(S, Type).

Functions are closure-typed (and their "type" captures the current type environment, which is a weird type, maybe?)::

typical(fn(Name, Body), closure(Name, Body, Env)) -->
    close_over(Env).

Application is a little gnarly because we want to work in the type environment of the closure, so we need a context-switching predicate ``switch_to//2`` (as ``switch_to/4`` but used as a DCG) that swaps the current type environment for the one you give it:

typical(apply(Fn, Arg), Type) -->
    typical(Fn, closure(Name, Body, Env)),
    typical(Arg, ArgType),
    switch_to(From, Env),
    type_put(Name, ArgType),
    typical(Body, Type),
    switch_to(_, From).

switch_to(From, To, From, To).

And we need to write ``type_put//2`` (as ``type_put/4`` but used as a DCG) to put type bindings in the environment:

type_put(Name, _, E0, _) :-
    get_assoc(Name, E0, _), !,
    write('name collision '),
    write(Name), nl,
    fail.

type_put(Name, Type, E0, E) :-
    put_assoc(Name, E0, Type, E).

All in all, I think this could be considered a kind of abstract evaluation. In any event, that's one way to write a type inferencer in Prolog.

Conclusion

test0(Source, VarList, Value) :-
    parse(Source, AST),
    list_to_assoc(VarList, Variables),
    empty_assoc(Functions),
    meaning(AST, Value, Functions, Variables).

Which allows us to check the semantics of code fragments by "injecting" variables into the variable binding environment:

?- test0(`a * b`, [a-23, b-14], Value).
Value = 322 .

?- test0(`a * b`, [a-23, b-B], Value).
23 * B #= Value .

Hamel goes on to prove things about bits of code using Prolog as a proof assistant.