The Extol Programming Language

We are building a programming that will have:

A uniform language for values, expressions, types, kinds, macros, patterns and tactics
Unrestricted predicates, constraint-solving, proofs and first-class patterns as core building blocks
A composable effects system that allows chosing abstraction levels and hides all lower abstractions
An extensible grammar that allows heavily bikeshedded coding styles
A compiler and a parser which are entirely generated from the interpreter and the AST data type
An FFI that can import and export to and from C, C++, Python, JavaScript, Ruby, Perl, sh, Java, .NET, Go, Rust, R, ELisp and Nix

Documentation

Examples

Some day Extol code might look like this, with inferred types checked at compile-time:

define fib
  0: 1
  1: 1
  n: fib (n - 1) + fib(n - 2)

But today look like this, and the types are checked at runtime:

define fib:
    arguments(N),
    returns X,
    requires number(N),
    ensures number(X),

    (0: 1),
    (1: 1),
    (N: fib(N - 1) + fib(N - 2)).

Arbitrary Prolog-style predicates can be used as types, such as these types used by the compiler:

pred declaration:
    (define(Name, Annots, Clauses):
        atom(Name),
	maplist(annotation, Annots),
	maplist(define_clause, Clauses)),
    (test(Name, Goals):
        atom(Name),
	goal(Goals)).

pred annotation:
    (nondet: true),
    (predicate: true),
    (returns(Var): true),
    (ensures(Pred): xtl_goal(Pred)),
    (requires(Pred): xtl_goal(Pred)),
    (traced: true),
    (dcg: true),
    (parameters(List): maplist(var, List)).

There is support for declarative grammars such as this parser for Extol terms:

dcg xtl_regular_term:
((Char) : "0'", !, require(xtl_string_char(Char)), xtl_skipwhite),
((Integer) :
    many1(digit, Ds), !,
    { foldl(add_digit, 0, Ds, Integer), ! },
    xtl_skipwhite),
((String) : "\"", !, require(many(xtl_string_char, String)), require("\""), xtl_skipwhite),
((Term) :
    xtl_atom(Atom), !,
    ( xtl_token("("), !,
      xtl_comma_separated(Args, [], xtl_token(")")),
      { Term =... [Atom | Args] }
    ; xtl_skipwhite,
      { Term = Atom })),
% ...

With a built-in test framework that allows writing tests like this:

test xtl_regular_term :
    xtl_regular_term(123, "123", ""),
    xtl_regular_term(hi, "hi", ""),
    xtl_regular_term(hi(1), "hi(1)", ""),
    xtl_regular_term(hi(b, 4), "hi(b, 4)", ""),
    % ...

Quick Start

Setup Extol

Get the latest source code:

git clone https://github.com/extollers/extol
cd extol

Install the dependencies. For example, on Ubuntu:

sudo apt install gprolog

Or with Nix:

nix develop

Build the compiler and install it to ./local:

make install

Using the REPL

$ ./local/bin/extol repl

Extol> 1 + 1
2

Extol> 'Hello, world!'
Hello, world!

Using the compiler

$ cat > hello.xtl
pred main: ():
  write('Hello, world!'), nl,
  halt.

$ ./local/bin/extol extoltoprolog hello.xtl hello.prolog

$ gplc hello.prolog

$ ./hello
Hello, world!

Inspiration

Extol is inspired in part by the following languages and tools:

Mercury: Combining the power of Haskell and Prolog
CiaoPP: Type inference, static debugging and program transformation as a preprocessor
Picat and Rosette: Constraint solving as a primitive
Lean: A common language for programming, metaprogramming and theorem proving
Cecil: Predicate objects
Swig: Automatically generated glue code for interfacing with other languages

Roadmap