🦊 The Phox Programming Language

Phox is a small functional programming language.

It aims to be a simple yet expressive tool - your clever companion for exploring type theory and practical programming.

✨ Features

• Hindley–Milner type inference
  No need to annotate types in most cases.
  (Phox includes a minimal type-annotation syntax for expressions, used only when disambiguation is needed.)
• Algebraic data types (ADT)
  Define expressive data structures with variants.
• Pattern matching
  Concise and powerful destructuring.
• Newtype shorthand
  Cleaner syntax for single-constructor wrapper types.
• First-class functions
  Functions are values, operators are functions too.
• Generic function temlates
  Non-first class / overloadable generic function templates.
• Multi-parameter typeclasses (trait/impl)
  Define the relationship between multiple methods and multiple types.
• Trait record
  Typeclasses (trait/impl) can be instansiated as a first-class record value, with a simple syntax.
• Module system
  Rust like module / namespace definition.
• Simple syntax
  Inspired by ML-family languages, with a focus on clarity.

Install Phox

⚠️ Work in progress — Phox is under active development.

Build

Clone the GitHub repository and build with Rust (tested on 1.80+, may work on earlier versions):

git clone https://github.com/mori0091/phox.git
cd phox
cargo build

Run in REPL

If you run without arguments, Phox starts an interactive REPL:

cargo run
> let rec fact = λn. if (0 == n) 1 else n * fact (n - 1);
> fact 5
=> 120: Int

In REPL, an input starts with : is recognized as a REPL command.
For example, :? shows the list of available commands:

cargo run
> :?

:quit, :q
    exit REPL.

:help, :h, or :?
    print this help messages.

:load <path>, :l <path>
    load and evaluate Phox source file specified by <path>.

:modules, :m
    print list of root modules.

:using, :u
    print list of using aliases for each modules.

:symbols, :s
    print list of symbols for each modules.

:impls, or :impls [options]
    print list of `impl`s.
    options:
        -v, or --verbose
            print also the `impl`s' implementation.

Run a program file

Pass a .phx file to execute it:

• .phx is the conventional extension for Phox source files (plain text).
• .txt files are also accepted.

cargo run examples/fact.phx
=> 120: Int

Run from stdin

You can also pipe code from stdin (use - explicitly):

echo "1 + 2" | cargo run -
=> 3: Int

Resulting value and inferred type are printed on success, like this:

=> value: type

On error, an error message is printed, like this:

parse error: UnrecognizedToken { /* snip... */ }

First Program

> println "Hello World!"
Hello World!
=> Ok (): Result Error ()

> println ("Hello" ++ " " ++ "World!")
Hello World!
=> Ok (): Result Error ()

> println <| fmt::show <| fmt::sep_by "_" <| "Hello World!"
H_e_l_l_o_ _W_o_r_l_d_!
=> Ok (): Result Error ()

Note

Phox is still under active development.
While most I/O primitives have not yet been implemented, but the following core features are already available:

• Type-level Unicode String Framework (ScalarString, UTF-8, etc.)
• Pretty-Printing Combinators
• Rich pure-functional core libraries (iter, array, fmt, …)
• Experimental print, println, eprint, and eprintln

Pipeline Example

Iterator / Generator / Sink pipelines

> counter 1 |> take 5 |> fold (+) 0
=> 15: Int

> counter 1 |> take 10 |> fold (+) 0
=> 55: Int

> counter 1 |> take 5 |> fold (*) 1
=> 120: Int

> counter 1 |> filter (|(% 2) >> |(== 0)) |> take 5 |> collect Nil
=> Cons 2 (Cons 4 (Cons 6 (Cons 8 (Cons 10 Nil)))): List Int

> counter 1 |> filter (|(% 2) >> |(== 0)) |> take 5 |> collect @[]
=> @[2, 4, 6, 8, 10]: @[Int]

> collect "abc" "def"
=> "abcdef": ScalarString

> "abc" ++ "def"
=> "abcdef": ScalarString

> @[1,2,3] ++ @[10,20]
=> @[1, 2, 3, 10, 20]: @[Int]

> "Hello" ++ " " ++ "World"
=> "Hello World": ScalarString

Note

The infix operator ++ is synonym of collect function.

Pretty-Printing combinator pipelines

> use ::core::fmt::*;
=> (): ()

> show <| hex-dump <| cast "🎉🤣👍🍺"
=> "F0 9F 8E 89 F0 9F A4 A3 F0 9F 91 8D F0 9F 8D BA": ScalarString

> show <| sep_by ", " <| map single-quote <| "🎉🤣👍🍺"
=> "'🎉', '🤣', '👍', '🍺'": ScalarString

Note

The ::core::fmt module is not imported by default.
You must either:

• call functions with a module path such as fmt::show, or
• explicitly import the module with use ::core::fmt::*;

Comments

Line comments

In regular expression: //[^\n\r]*

• starts with //, followed by any characters (single-line text), and ends with newline.

// This is a line-comment.

////// This is also a line-comment.

Similar to C/C++ line-comments.

Block comments

In regular expression: /\*[^*]*\*+(?:[^/*][^*]*\*+)*/

• starts with /*, followed by any charcters (single or multi-line texts), and ends with */.
• Nesting is not allowed.

/* This is a block comment. */

/*
 * This is also a block comment.
 */

/*****
 *** This is also a block comment.
 **/

Similar to C/C++ block-comments.

Semicolon (item separator)

• ; separates multiple items (declarations / statements / expressions) in a block or at the top level.
• Each item is evaluated in order; only the last expression’s value is returned.
• If a block or top-level input ends with ;, an implicit () is added.

// Multiple items in a block
{
    let x = 1; // => (): ()  (discarded)
    let y = 2; // => (): ()  (discarded)
    x + y;     // => 3: Int  (discarded)
    2 * x + y  // => 4: Int  (result)
}
// => 4: Int

// Multiple items in the top level
let x = 1; // => (): ()  (discarded)
let y = 2; // => (): ()  (discarded)
x + y;     // => 3: Int  (discarded)
2 * x + y  // => 4: Int  (result)
// => 4: Int

// Items in a block ends with `;`
{
    1 + 2; // => 3: Int  (discarded)
}
// => (): ()

// Items in the top level ends with `;`
1 + 2; // => 3: Int  (discarded)
// => (): ()

// No items in a block
{}
// => (): ()

Primitive Types

Note

ScalarString is synonym of Str ScalarValue type.

Type definitions

type Option a = Some a | None;
type Pair a b = Pair a b;
type Result e a = Ok a | Err e;

• Variants can take 0 or more arguments.
• Newtype shorthand is available when:
  • There is only one variant, and
  • The type name and constructor name are the same, and
  • The variant has exactly one tuple, one record, or one array argument.

// Normal form
type Point a = Point @{ x: a, y: a };
type Wrapper a = Wrapper (a,);

// Newtype shorthand
type Point a = @{ x: a, y: a };
type Wrapper a = (a,);

Language constructs

Identifiers

Variables and type variables

In regular expression:[a-z_]([-]*[a-zA-Z0-9_]+)*['?]*

• seq, x', some?, foo-bar
• fooBar, a0, take_while

Constructor, type constructor, and trait names

In regular expression:[A-Z][a-zA-Z0-9_]*

• List, Nil, Eq, Iter

Module names

In regular expression:[a-z_]([-]*[a-zA-Z0-9_]+)*

• core, cmp, iter

Module path (qualified module names)

A sequence of module names separated by ::

• ::core::cmp, ::core::list Absolute path
• cmp, list, foo::bar Relative path

Qualified names

A module path followed by a variable, constructor, type constructor, or trait name

• ::core::iter::seq, ::core::iter::Seq, ::core::iter::Iter
• iter::seq, iter::Seq, iter::Iter

Literals

• () Unit value literal
• true, false Boolean value literals
• 0,100, -1 Integer value literals
• 0u8, 100u8, 0xFFu8 8-bit unsigned integer literals
• 0u16, 100u16, 0xFFFFu16 16-bit unsigned integer literals
• 0u32, 100u32, 0xFFFFFFFFu32 32-bit unsigned integer literals
• 0u64, 100u64, 0xFFFFFFFFFFFFFFFFu64 64-bit unsigned integer literals
• 'A', '\n', '🎉' Unicode Scalar Value literals
• "abc", "🎉🤣👍🍺" Unicode UTF-8 string literals

Primitive types

• () Unit type
• Bool Boolean type
• Int Integer type
• u8 8-bit unsigned integer type
• u16 16-bit unsigned integer type
• u32 32-bit unsigned integer type
• u64 32-bit unsigned integer type
• ScalarValue Unicode Scalar Value type
• ScalarString Unicode UTF-8 string type (synonym of Str ScalarValue)
• @[t] or @[] t Array type
• (t,), (t1, t2) Tuple type
• @{x:t1, y:t2} Record type
• t1 -> t2 Function type
• T t, t1 t2 Type-level function application

Operators

Infix (binary) operators

• ==, != Equality / Non-equality operators
• <=, <, >, >= Comparison operators
• &&, || Logical operators
• +, -, *, /, % Arithmetic operators
• |>, <| Pipeline operators
• >>, << Function composition operators

Prefix operators

• nagete, - Arithmetic negation
• not, ! Boolean not

User defined infix operators

In regular expression:[*+\-/!$%&=^?<>]+

• ?>, ===, <+>

Operators as functions

• (==) 1 1
• (+) 1 2

Functions and constructors as operators

• 1 `Cons` Nil
• x `@{Eq Int}.(==)` y

Declarations

At the top level of a module:

• mod Define sub-module
• use Import identifiers
• type Define Algebraic Data Type (ADT)
• trait Define Multi-Parameter Type Class (MPTC)
• impl Define MPTC instance implementation
• *let Define generic/overloaded function template
• let Define a variable or function
• let rec Define a recursive function

Statements

Within a local scope:

• let Variable / function binding
• let rec Recursive function binding

Note

In the case of let rec p = e;,

• p must be a variable pattern.

In the case of let p = e;,

• At the top level of a module, p must be a variable pattern.
• Within a local scope, any pattern can be used for p.

Expressions

Value expressions

(evaluate to themselves; safe to generalize)

• (), true, 0 Literals
• λp.e/\p.e Lambda abstraction (function)
• @[], @[e1], @[e1, e2] Array value
• (e1,), (e1, e2) Tuple value
• @{x = e1, y = e2} Record value
• @{T t1 t2} Trait record value
• |(e op)/|(e op _) Infix-operator partial application (bind the 1st argument)
• |(op e)/|(_ op e) Infix-operator partial application (bind the 2nd argument)

Infix-operator partial applications (a.k.a. section syntax) are desugared into lambda abstraction.

Note

Old section syntax #(e op)/#(e op _) and #(op e)/#(_ op e) are deprecated.
Use new syntax |(e op)/|(e op _) and |(op e)/|(_ op e) instead.

Important

Old record value syntax @{x: e1, y: e2} are deprecated and no longer supported.
Use new syntax @{x = e1, y = e2} instead.

Non-value expressions

(require evaluation; not eligible for generalization)

• x Evaluate variable
• e1 e2 Function application
• e1[e2] Array index access
• e.0 Tuple index access
• e.x Record field access
• { stmt1; stmt2; expr } Block expression (evaluates to the last expression; introduces a new scope)
• if (e1) e2 else e3 If then else
• match (e) { p1 => e1, .. } Pattern matching

Minumul Type Annotaions

• e: t Optional type annotations for expressions
  This adds a type equality constraint between the inferred type of e and the annotated type t.
  This helps type inference and the constraint solver resolve the last mile of ambiguity.

• Type annotations as signatures are required only in trait declarations.
  Other bindings (such as let and lambda parameters) do not accept type signatures.

Note

The expr: t syntax is only permitted for atomic expressions.
If you need to type-annotate a complex expression,
enclose the expression in parentheses and follow it with the type annotation.

Examples:

let add = \a.\b. (a + b): Int;

add 2 + 3
// => 5: Int

(cast 10): u8
// => 10: u8

(cast 10): (Result e u8)
// => Ok 10: Result RuntimeError u8

Patterns

• _ Wildcard pattern
• (), true, 0 Literal pattern
• 'A', '🎉' Unicode Scalar Value literal pattern
• x, foo Variable pattern
• Nil, Cons p ps Constructor pattern
• @[], @[p1, p2], @[p, ps..], @[p, ..], @[ps..], @[..] Array pattern
• (p1,), (p1, p2) Tuple pattern
• @{x = p1, y = p2}, @{x, y} Record pattern

Important

Old record pattern syntax @{x: p1, y: p2} are deprecated and no longer supported.
Use new syntax @{x = p1, y = p2} instead.

Phox Design Principles

See widely.
Think deeply.
Step back, breath, and see widely again.
It’s okay? then
Build simply.

Appropriate structure should make desired properties emerge.

Don’t add. Polish. Compose.

Every element that makes up Phox ‐ including its concept, syntax, semantics,
type system, run-time system, abstract machine, and standard library ‐
should satisfy all six of the following principles:

1. High purity
2. Orthogonality
3. Clarity
4. Simplicity
5. Predictability
6. Theoritical optimality

Complexity must be eliminated, not accommodated.

Phox is not so easy, but
Phox must be kind to both humans and machines.

No magic. Be gentle.

[WIP] Async-Computation and Async I/O

An asynchronous task ≒ VM instance.
(The Phox VM itself is a state-machine based on Suspendable Term Reduction Abstract Machine (STReAM))

An asynchronous task is executed by a dedicated VM instance.
Each VM instance is a single-threaded execution context.
Multiple VM instances may be executed in concurrently by dedicated threads.
(depends on scheduler implementations)

User-defined tasks

Define task constructors:

• Task constructor name must end with &
• Task constructors are uncurried
• task(args..) {...} is task constructor abstraction

*let foo& = task(x) {...};
*let bar& = task(x,y) {...};
*let download& = task(url) {...};

Constructs a task:

• A call to a task constructor constructs a task abstraction.
• A task abstraction (or simply “task”) of type Task a wraps an expression e of type a,
  where e is the task constructors’ body.
• The expression e is not evaluated immediatelly.

let tsk = download&(url);

Schedule a task and instantiate the corresponding job:

let job = schedule _DEFAULT_SCHEDULER_ tsk;

Await the job completes and take result:

let res = await job;

Async-APIs and semantics

• schedule : sc -> Task a -> JobHandle a

  schedule sc t

  • schedule sc t schedules task t to scheduler sc.
    • That constructs a dedicated VM instance for the task t, and
    • returns corresponding job-handle of type JobHandle a.
  • The job is registered to the scheduler’s runnable-queue, then
    • an executor will be assigned to a runnable job, and
    • the executor executes (start/resume) the corresponding VM instance.

• await : JobHandle a -> Result Error a

  await job

  • If the job has already finished, returns Ok val where val is its resulting value of type a.
  • If the job has already canceled, returns Err err.
  • Otherwise,
    • registers the current job to wait-queue of the job,
    • and suspend the current job.
  • When a job is finished,
    • Ok val is passed to all jobs waiting in its wait-queue,
    • and awake them. (i.e. schedule them again)
    • the wait-queue shall be cleared.

• cancel : JobHandle a -> ()

  cancel job

  • If the job has already finished or canceled, returns ().
  • Otherwise,
    • mark the job as canceled, then
    • Err err is passed to all jobs waiting in its wait-queue,
    • and awake them. (i.e. schedule them again)
    • the wait-queue shall be cleared.

Note

• task/schedule/await/cancel control the evaluation strategy and order of expressions.
• task/schedule/await/cancel themselves are not “operations with side effects.”
• Asynchronous I/O would be implemented using the proc-system, such as task (proc! {...}).

rough sketch

trait Cancel h a {
    cancel : h a -> ();
};

trait Await h a {
    await : h a -> a;
};

trait TryAwait h a {
    await : h a -> Result Error a;
};

trait Schedule sc a {
    schedule : sc -> Task a -> JobHandle a;
};

// -------------------------------------------------------------
impl Cancel JobHandle a {
    cancel = __cancel_job__;
};

impl TryAwait JobHandle a {
    await = __try_await_job__;
};
impl Await JobHandle a {
    await = \job. match (@{TryAwait JobHandle a}.await job) {
        Ok x => x,
        // _ => /* runtime error */
    };
};

type DefaultScheduler = @{ /* ... */ };

impl Schedule DefaultScheduler a {
    schedule = __schedule_job__;
};

let _DEFAULT_SCHEDULER_ = DefaultScheduler @{ /* ... */ };

// let t = ... ;             // t : Task a
// let job = schedule sc t;  // job : JobHandle a
// `await job |> (\Ok x. x)`   // => `@{TryAwait h a}.await` is performed
// `await job |> (\x. x + 1)`  // => `@{Await h Int}.await` is performed

#![allow(unused)]
fn main() {
// === Representation of Job in runtime-system. ===
type JobHandle = Rc<RefCell<Job>>;
enum Job {
    Canceled,        // => Err err
    Done(vm::Term),  // => Ok val
    InProgress {
        state: vm::State,
        waiters: Vec<JobHandle>,
    },
}
}

[WIP] Proc System: A Separate World for Controlled Mutation

Phox separates pure and procedural worlds at the type and syntax level.

Procedural types

Procedural types (DynArray! a, Slice! a, Ptr! a, …) represent mutable data structures used only inside procedural blocks.

• cannot escape into the pure world
• pure functions cannot observe or depend on them
• they exist only as temporary mutable views created via thaw!
• they must be converted back to pure values via freeze!

Procedural types are always local to a single VM instance and never shared.

proc! {
    let buf = thaw!(xs);     // @[a] → DynArray a
    do_inplace_operation!(buf);
    freeze!(buf)             // DynArray a → @[a]
}

User-defined procedures

Define procedures:

• Procedure name must end with !
• Procedures are uncurried
• proc(args..) {...} is procedure abstraction

*let foo! = proc(x) {...};
*let bar! = proc(x,y) {...};
*let download! = proc(url) {...};

Procedure call (only allowed inside proc! { ... }):

proc! {
  foo!(1);
  bar!(2,3);
  ()  // `proc! {...}` must return a **pure** value
};

let x = proc! { download!(url) };

Resource types

Resource types represent opaque handles to external OS resources.

• can escape into the pure world
• pure functions cannot observe or pattern-match them
• operations on resource values are allowed only in proc world
• each resource type defines a destructor drop!
• drop! is called automatically when the reference count becomes zero
• drop! cannot be called explicitly

Resource values may be shared within a single VM instance without mutual exclusion,
because procedural types never escape and pure values are immutable.

Note

Resource types are builtin and provided only by the runtime system.
Users cannot define new resource types.

// ----
// The following `resource ... drop! ...` syntax is **illustrative only**
// and does not exist in the actual language:
// ----
// Define resource type.
// - Resource name must end with `!`
// - Resource type has exactly one constructor of the same name
// - Resource type has exactly one destructor `drop!`
// - `drop!` is called automatically when Rc becomes 0
// - Construction and pattern match are allowed only in proc world
resource MyResource! a = @[a]
drop! = proc(MyResource! xs) {
  ...
};

Concurrency and VM instances

Each VM instance is a single-threaded execution context.

• procedural types never escape
  → no shared mutable state
• pure values are immutable
  → safe to share
• resource values are opaque
  → safe to share as long as operations are restricted to proc world
  and isolated within VM boundaries

Only the await operation can transfer resource values between VM instances.

This means:

• resource sharing/movement happens only at await boundaries
• mutual exclusion is required only for resource operations that cross VM boundaries
• no mutual exclusion is needed inside a single VM instance

If the job’s return value does not contain a resource value,
there is no limit on the number of waiters.

Otherwise, Phox limits the number of waiters for a JobHandle a to 1 at most.
In this case, await job consumes the resource returned by job (ownership transfer), and any subsequent calls to await job will result in an error.

Note

Resource operations may interact with external OS resources.
External resources are not pure and may cause race conditions.
Phox guarantees safety inside the VM, but external resource conflicts
must be handled by appropriate OS-level APIs (e.g., file locks).

Opacity of Resources and Transparency of Resource Ownership

Resource-type values are opaque.
However, resource ownership must be structurally visible and transparent.

To prevent resource leaks,
Phox restricts the encapsulation of resource values within opaque structures.

Specifically:

• Closures cannot cross the VM boundary.
• Any values containing closures cannot cross the VM boundary.

Therefore, await job can return the following:

• ADTs, Arrays, tuples, or records that do not contain closures,
• Resource values, or
• Primitive values.

Rules for Transparency of Resource Ownership

• Resource Inflow Violation Rules:

  • Values bound by top-level let/let rec must be resource-free
  • Values passed to a task constructor as its arguments must be resource-free.
    These values will be bound to the initial environment of the corresponding job.
  • The initial environment of a job contains the task’s arguments only.
    (resource-free environment)
  • And job can access to the top-level/global environment.
    (resource-free environment)

• Resource Outflow Violation Rules:

  • The return value of await job must be resource-transparent

• Resource Sourcing Violation Rule:

  • The return value of proc!{...} must be resource-transparent
    if such expressions exist in top-level let/let rec bindings.

where:

• resource-free means

  The value must not contain any resource values

• resource-transparent means

  The value must not contain any opaque structures, such as closures
  (This prevents resources from being hidden inside ADTs or closures.)

Note

In other words,

• Top-level let/let rec bindings must be resource-free:
  their right-hand-side expressions (and all subexpressions) must not construct resource values.
• A call to the task constructor must be resource-free.
  The expression passed as its argument (and all its sub-expressions) must not contain any resource values nor opaque structures.
• The return value of await job (i.e. the resulting value of a task) must be resource-transparent.

Open issues

Note

TODO: Phox must detect and eliminate cases where top-level let/let rec bindings contain resource values by recursively checking the AST.

The below is the typical case:

// `r` is a resource value.
let r = proc!{ open_file!("foo.txt") };

// λ expression that captures resource `r`.
let f = \x. proc! { write!(r, x); };

// Note that value structure of type `MyADT a` is opaque for the type system.(!)
// ADT values can encapsulate closures. (resource `r` leaks!)
type MyADT a = MyADT (a -> ());
let v = MyADT f;

Note

T.B.D.: Phox may restrict use of proc! {...} only for *let template definitions.
This can eliminate most miss-usecases like the above in the language syntax-level.

See also Structural Transparency of Types (STraT).

[WIP] Structural Transparency of Types (STraT)

Structural Transparency of Types (STraT) is an attribute of types.

Definition

enum StructuralTransparency {
  Opaque,                             // the type is opaque
  SemiTransparent { ts: Vec<Type> },  // transparency of the type depends on transparency of `ts`.
  Transparent,                        // the type is transparent
  Any,                                // transparency is not determined (for fresh type variable)
}

• Function types (closures) are Opaque.
• Primitive types are Transparent.
• Procedural types; such as dynamic arrays; are Opaque.
  (Meaningless because they cannot escape to pure world and cannot cross the VM boundary)
• Resource types; such as file-handle; are Transparent.
  (Though its value structure is opaque, the run-time system ensures that it contains no other resources nor closures)
• Tuples, Arrays, Records are:
  • Opaque if an element type was Opaque,
  • Transparent if all element types were Transparent,
  • SemiTransparent otherwise.
• ADTs are:
  • Opaque if an element of any variant was Opaque,
  • Transparent if all element types of all variants were Transparent,
  • SemiTransparent otherwise.
• Fresh type variables are Any.
  (Their transparency is determined via type unification process)

Example

• a is Any (if not unified yet)
• a -> b is Opaque.
• Int is Transparent.
• File! is Transparent. (resource types)
• Option Int is Transparent.
• Option File! is Transparent.
• Option a is SemiTransparent { ts: vec![a] }.
• Result e a is SemiTransparent { ts: vec![e, a] }.
• Map s a b is Opaque. (because its data constructor is Map (a -> b) (s a))

Unification

If type t1 and t2 are successfully unified (unify(t1, t2) succeeded),
their STraT attributes are merged.

• merge(X, Opaque) = Opaque
• merge(Opaque, X) = Opaque
• merge(Transparent, Transparent) = Transparent
• merge(Transparent, SemiTransparent{A}) = SemiTransparent{A}
• merge(SemiTransparent{A}, Transparent) = SemiTransparent{A}
• merge(SemiTransparent{A}, SemiTransparent{B}) = SemiTransparent{A ∪ B}
• merge(X, Any) = X
• merge(Any, X) = X

In other words, the unification of STraT corresponds to the maximum (join) of the following partially ordered set (poset):

Opaque > SemiTransparent > Transparent > Any

Type Constraints

• ResourceFree = “No resource value”
• ResourceTransparent = “No opaque values that hide resources”

By definition, a resource type is transparent as a type but opaque as a value.

In contrast, ResourceFree and ResourceTransparent are type-constraints that
ensure the type system can reliably check for transparency of resource ownership.

ResourceFree type-constraint

The constraint ResourceFree(ty) is:

• if ty was Opaque:
  • ResourceFree(ty) causes an error.
• if ty was Transparent:
  • ResourceFree(ty) causes an error, if the ty itself or its type-parameters contain resource types.
  • ResourceFree(ty) is OK, otherwise.
• if ty was SemiTransparent{ts: vec![a, b, ...]}:
  • ResourceFree(ty) causes an error, if the ty itself or its type-parameters contain resource types.
  • ResourceFree(ty) is ResourceFree(a) ∧ ResourceFree(b) ∧ ..., otherwise.

ResourceTransparent type-constraint

The constraint ResourceTransparent(ty) is:

• if ty was Opaque:
  • ResourceTransparent(ty) causes an error.
• if ty was Transparent:
  • ResourceTransparent(ty) is OK.
• if ty was SemiTransparent{ts: vec![a, b, ...]}:
  • ResourceTransparent(ty) is ResourceTransparent(a) ∧ ResourceTransparent(b) ∧ ....

STReAM: Suspendable Term Reduction Abstract Machine (overview)

1. Introduction

We present STReAM, the Suspendable Term Reduction Abstract Machine designed for the strict functional language Phox.
Although STReAM shares superficial similarities with classical machines such as the Krivine Machine, CEK, SECD, and STG, it diverges fundamentally through:

• strict (eager) evaluation,
• heap-first value representation,
• a two-layer structure of lexical vs. continuation environments,
• continuation sequencing via CSeq,
• a step-based reduction loop that flattens AST nodes,
• and a fully suspendable VM state.

STReAM is therefore a new species of abstract machine, not reducible to any existing model.

2. Machine State

STReAM decomposes its state into three semantic scopes:

• lexical scope : the current term and its lexical environment
• contextual scope : continuation code and continuation values
• global scope : global code table and heap

2.1 Formal State

VM state = (term, ctx.conts, ctx.env, g.codes, g.heap)

#![allow(unused)]
fn main() {
State {
  term : Term,        // lexical scope
  ctx  : Context {    // continuation scope
    conts: CStack,
    env:   Env,
  },
  g : {               // global scope
    codes: GlobalEnv,
    heap:  Heap,
  },
}
}

Note
term and ctx are specific to each VM instance,
while g may be shared across multiple VM instances.

Thus, STReAM naturally supports asynchronous and concurrent execution
at the abstract machine level.

3. Instruction Set

3.1 Expressions

App(M, N)
CSeq(M, N)
LetRec(X, E)
Var(n)
GlobalVar(s)
For
Match(scrut, arms)
IndexAccess(t, i)
TupleAccess(t, n)
FieldAccess(t, label)

3.2 Value Constructors

Lit(L)
Tuple(n)
Con(name, n)
Record(labels)
Array(n)
ArrayU8(n)
...

3.3 Continuations

KApp
KMatch(arms)
KIndexAccess
KTupleAccess(n)
KFieldAccess(label)
KFor
KFor2
KLetRec(E)

4. Dynamics

STReAM’s run_state() always performs exactly one AST-flattening step,
and repeated application of this step drives evaluation.

4.1 WHNF (termination)

If ctx.conts is empty and term is WHNF (Lam or Val), evaluation terminates.

4.2 WHNF with continuation

The current term is stored in the heap, its address is pushed to ctx.env,
and the next continuation is loaded.

4.3 CSeq (Continuation Sequencer)

CSeq(M, N)
→ push continuation N (as closure)
→ replace current code with M

This separates “evaluate M” from “then execute N” at the AST level.

4.4 ACCESS / APP / LETREC

Variable lookup, strict application, and recursive binding follow the formal rules
defined in the transition tables.

5. Comparison with Existing Machines

5.1 Krivine Machine

• shares closures and de Bruijn environments
• differs in strict evaluation and flattened continuations

5.2 CEK Machine

• similar continuation stack
• CEK continuations are recursive trees; STReAM continuations are flat sequences
• CEK lacks the three-layer environment model

5.3 SECD Machine

• S/E/C/D correspond structurally to STReAM’s components
• but STReAM uses AST + CSeq flattening instead of instruction lists

6. Suspend/Resume

Because STReAM’s state is fully linearized:

• suspend = copy the State
• resume = restore the State

This enables:

• async/await
• generators
• coroutines
• resumable pipelines
• concurrent VM instances

without modifying language semantics.

7. Conclusion

STReAM is a novel abstract machine characterized by:

• strict evaluation
• heap-first value representation
• AST-flattening semantics
• continuation sequencing via CSeq
• a three-layer environment model
• suspendable VM state

In summary:

“A strict, heap-first, flattening continuation machine with a three-layer environment model.”

STReAM does not match CEK, SECD, STG, ZINC, or Krivine.
It is a genuinely new architecture suited for modern language features such as async, pipelines, and pattern matching.

STReAM: Suspendable Term Reduction Abstract Machine (formal semantics)

• STReAM is Suspendable Term Reduction Abstract Machine designed for
  strict functional programming languages.
• Phox VM is an implementation of STReAM designed for
  the Phox programming language.
• Phox is a strict functional programming language.

Machine State

STReAM decomposes its state into three semantic scopes:

• lexical scope : the current term and its lexical environment
• contextual scope : continuation code and continuation values
• global scope : global code table and heap

Formal State

VM state = (term, ctx.conts, ctx.env, g.codes, g.heap)

State {
  // lexical scope
  term : enum Term {
    Val(Value),       // a value, or
    Clo(Closure {     // a closure
      code: Code,     // - code of the closure
      env: Env,       // - variables bounded to the closure
    }),
  },
  // contextual scope
  ctx : Context {
    conts: CStack,    // continuation closure-stack
    env: Env,         // continuation value-stack
  },
  // global scope
  g : {
    codes: GlobalEnv, // global code table
    heap: Heap,       // global store
  },
}

Note

term and ctx are specific to each VM instance, but
g is sharable among multiple VM instances.

In other words,

• By their very nature, one VM instance can represent one suspendable tasks or jobs, and
• Multiple VM instances (i.e., multiple tasks/jobs) can run in concurrent, if the global allocator g.heap is multithread-safe,

Consequently, the STReAM/Phox VM can naturally support asynchronous and concurrent computation at the abstract machine and runtime system levels.

Notations of VM state

• term

  Term. A Term is Closure or Value.

  • t means an arbitrary Closure or Value.
  • <val> means an arbitrary Value.

    • val

      Value

      • …
  • {code, env} means a Closure. Closure is pair of Code code and Env env.

    • code

      Code (Instruction)

      • Lit L | Var n | Lam E | App M N | …

    • env

      Environment stack (Env)

      • [] means empty Env.
      • es means an arbitrary Env.
      • a::es means an Env whose top is a, where a is an address of heap
      • es[n ↦ a] means Env es whose element at de Bruijn index n is address a

• ctx.conts

  Continuation closure-stack (CStack)

  • [] means empty CStack
  • ks means an arbitrary CStack.
  • k::ks means a CStack whose top is k, where k is a Closure.

• ctx.env

  continuation value-stack (WStack ≡ Env)

  • [] means empty WStack
  • ws means an arbitrary WStack.
  • a::ws means a WStack whose top is a, where a is an address of heap

• g.codes

  Random access read-only code table. (GlobalEnv)

  • gs means an arbitrary GloalEnv.
  • gs[s ↦ c] means GloalEnv gs whose element at key s is code c

• g.heap

  Random access heap memory (Heap)

  • h means an arbitrary Heap.
  • h[a ↦ t] means Heap h whose element at address a is term t
  • h[a ↦ {}] means heap h whose element at address a is nil
    (i.e. a is fresh address to be allocated later)

Note

h[a ↦ {}] does not allocate memory.
It only denotes that a is a fresh address.
Actual allocation occurs when a value is written to a.

Dynamics of VM state transition

• WHNF (end of state transition)
• WHNF w/ continuation
• CSEQ (Continuation Sequencer)
• ACCESS (variable lookup)
• APP (function application)
• LET (let binding)
• LETREC (recursive binding)

WHNF (end of state transition)

Evaluation halts when the current term was {Lam E, es} or <val> and there is no continuations.

WHNF w/ continuation

Save the current term to the heap, push its address to ctx.env, and load the next continuation.

• Allocate fresh address a of heap for the current term,
• Push a to ctx.env,
• Pop continuation from ctx.conts.

CSEQ (Continuation Sequencer)

• CSeq M N

  Evaluate M, and then N.
  Since N is evaluated after M,
  N is pushed onto the continuation stack as a closure, and
  the current code is replaced with M.

• Push continuation code N (as closure {N, es}) to ctx.conts,

• Replace the current code with M.

ACCESS (variable lookup)

• Var n

  Load term of a variable bounded the current env.

If de Bruijn index n was out of bounds, causes run-time error “variable not found”.

APP (function application)

• App M N

  Evaluate M and N in order, then apply the resulting function to the argument via KApp.

where:

• {Lam E, es} = resulting term (WHNF) of {M, es} via cont transition
• tN = resulting term (WHNF) of {N, es} via cont transition

LET (let binding)

The code Let X E is synonym of App (Lam E) X.

LETREC (recursive binding)

• LetRec X E

  Allocate a dummy for recursive binding, evaluate X, then update the dummy with the result and evaluate E.

where:

• dummy = an arabitrary allocated dummy term.
• f = an address that
  • holds dummy at first via letrec transition, and then
  • be updated with term at x later via kletrec transition.
  • finally f holds tX (the recursive function body).
• tX = resulting term (WHNF) of {X, f::es} via cont transition

🧭 Roadmap

✔️ Mission 1

• Hindley-Milner type inference
• Safe subset of System Fω
• Algebraic Data Type (ADT)

✔️ Mission 2

• Traits a.k.a., Type Class
• Trait Record - Type Class as first-class record value

✔️ Mission 3

• Multi-Parameter Type Class (MPTC)
• Higher-order Trait Record - MPTC as first-class record value
• Overloaded Function Template
• Type and requires inference w/o type annotation

Extra Mission 1

• Safe and Unsafe numeric conversion
• Array, String type
• Pretty-Printing Combinators
• Stream for Parser Combinators
• Parser Combinators
• Safe Type Family (type trait/type impl)
• String Family Literals

Extra Mission 2 - Proc system

• Procedures with side-effects
• Dynamic arrays (mutable / growable arrays)
• Standard I/O
• File I/O
• Async-Computation and Async I/O combinators

Extra Mission 3 - Optimization

• Unboxed arrays (for non-primitive types)
• Object file, Link-Loader
• Alias analysis and reuse analysis of heap memory.
• LLVM IR code generator.

It’s a long, long journey…

🏁 Goal

• Hello World!

> println "Hello, world! (Finally, we meet!)";
Hello, world! (Finally, we meet!)
=> (): ()