The Extol Programming Language

The Extol programming language is an early work-in-progress. It is currently being bootstrapped from Prolog.

The goals of this project are:

A uniform language for values, function, statements, expressions, types, kinds, macros, patterns, constraints, grammars, tactics and proofs
A flexible syntax that allows building incrementally typed high-level shell-style scripts, low-level systems code and domain-specific languages
A type system with small-core verifiable theorem proving, incremental typing, deferred type errors, termination proofs, no universe hierarchy and separate types for compile-time (semantics) and run-time (representation)
Semantics that allow strict/lazy/reactive/mixed evaluation, value/reference/move parameters, prompt finalization, optional garbage collection, mutable/immutable/const/nondet/constraint variables, weak/lazy/mutable/immutable/serializable types, backtracking, (un)delimited continuations, resumable exceptions, static/dynamic polymorphism and static/dynamic/multiple dispatch
A composable environment and effects system that allows hopping between abstraction levels, powerful negotiated implicit arguments and detailed introspection of program requirements and behavior
A portable self-hosted interpreter and cross-compiler that targets x86_64, ARM, C, .NET, JVM, WebAssembly and SPIR-V
An FFI that can import and export to and from C, C++, Python, JavaScript, Ruby, Perl, sh, Java, C#, Go, Rust, R, ELisp and Nix
Parallel, distributed, heterogenous, symbolic and partial execution
Built-in cross-platform support for file IO, declarative UI, networking, HTTP, HTML, JSON, IPC, Unicode, math, times and dates, regular expressions, concurrency, string formatting, serialization, cryptography and testing
A module and packaging system for code sharing and re-use

Documentation

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

Optionally, run all tests:

make check

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:

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
Red: Multi-paradigm, multi-typing, full-stack, human-friendy language. Fun guaranteed.

extollers/extol