DEV Community: Ryo Hirayama

For Macro Lovers: Could Tauto Have the World's Most Powerful Macro System?

Ryo Hirayama — Tue, 03 Nov 2026 00:00:00 +0000

Tauto combines a dependently typed proof system with a runtime featuring algebraic effects and ownership. This article introduces its macro system.

“The world's most powerful” is a bold claim for a title. The aim is to bring everything I want from macros into a single design:

Add new syntax and DSLs as libraries, complete with registered formatters and syntax highlighting.
Write macros that transform code based on its types and macros that build proofs, called tactics, using the same mechanism.
Keep expansion hygienic, so macros do not capture the caller's variables.
Run untrusted macros without giving them file access, without unbounded execution, and without compromising proof soundness.

Tauto on GitHub

Macros are ordinary functions that return syntax values
Macro kinds and when to use them
- Syntax macros: write in your own grammar
- Untyped macros: reinterpret an expression
- Typed macros: inspect types and context
- Tactics: macros that construct proofs
- Attribute macros: generate declarations
- Why list generated declarations?
Hygiene: macros do not capture the caller's names
Using effect analysis to contain macro execution
- What about infinite loops?
A powerful syntax-macro system
- Write a grammar, get a typed AST and parser
- Left recursion: LL(k) and LALR(1)
- Syntax errors report locations and expectations
- Registering formatters and syntax highlighting
- Embedding Tauto expressions in a grammar
- Build and prove a language implementation
More useful properties
- Every expansion can be traced
- Typed macros do not change the declaration environment
- Write typing judgments in a DSL
- Macro execution is ordered by file
Deliberate restrictions
Design priorities
What is not guaranteed
Summary

Macros are ordinary functions that return syntax values

Tauto macros are ordinary functions , rather than programs in a separate macro or template language. They take and return syntax values, represented by AST data types such as SynExpr and SynStmt, assembled with quote { … } and $x. Calls are always explicit: NAME!(…).

Whatever a macro produces, the expanded program goes through the same path as a handwritten program: the kernel and a second, independently implemented kernel. You do not need to trust the macro's generation logic to preserve type or proof soundness.

Macro kinds and when to use them

There are four kinds of macros. The function's input type alone determines the kind. There is no keyword such as typed macro.

Syntax macro: takes a typed AST generated from a grammar. Call it as name!(…) to introduce notation or a DSL.
Untyped macro: takes SynExpr. Call it as name!(a + b) to reinterpret an expression.
Typed macro: takes Judgement. Call it as name!(e) to transform code using its type and context.
Tactic: takes ProofStep. Call it as by name!(…): G { … } to automate proofs.

Syntax macros: write in your own grammar

A syntax macro parses its input using a grammar declared with syntax!. As an example, here is swap!, which swaps two variables.

syntax!(swp, ```
{% endraw %}
par
%start Pair
%%
Pair: Name Name;
Name: /[\p{L}_][\p{L}\p{N}_]*/;
{% raw %}

```) => struct Pair, fn parse

pub macro fn swap(p: swp::Pair): List(SynStmt) {
  let a := Syn::ident(p.name)
  let b := Syn::ident(p.name_2)
  quote stmts {
    let tmp := $a
    $a := $b
    $b := tmp
  }
}

The grammar lives in a fenced block tagged par. It automatically generates a typed AST called swp::Pair, which becomes the macro function's input.

After =>, the source lists the exact kinds and names of the declarations that will be generated. You do not need to write these lists by hand: tauto fmt --fill-generated main.taut fills in missing lists and corrects mismatched ones in that file and the files it imports, writing the results back to source.

The list is required for syntax!, inductive_syntax!, attribute macros, and other declaration-generating calls. Generating an unlisted declaration is an error, as is listing a declaration that is not generated. “Why list generated declarations?” below explains why the list remains explicit in the source.

Here is the caller:

import "swap.taut"
var tmp := 1
var other := 2
swap!(`tmp other`)
perform show("tmp", tmp)
perform show("other", other)


$ tauto macro expand main.taut
var tmp := 1
var other := 2
let tmp#1 := tmp
tmp := other
other := tmp#1
perform show("tmp", tmp)
perform show("other", other)

$ tauto run main.taut
tmp = 2
other = 1

The macro's temporary variable tmp becomes tmp#1, avoiding a collision with the caller's tmp. The #1 is a display name; when --write writes the expansion back to source, it becomes an ordinary name that does not collide. This illustrates the hygiene mechanism discussed below. You can inspect expansions at any time with tauto macro expand.

The DSL inside the backtick fences can also have its own formatter and syntax highlighting. Register the functions with with at the end of syntax!:

syntax!(swp, ```
{% endraw %}
par
…
{% raw %}

```, with(fmt: swp_fmt, tokens: swp_tokens)) => struct Pair, fn parse

fmt is called when tauto fmt formats the contents of a syntax literal such as swp…. tokens is called when the language server highlights it. The grammar author defines swp_fmt and swp_tokens as ordinary Tauto functions. Without registration, the contents are left unformatted and highlighting is inferred from terminal names. More details appear in “Registering formatters and syntax highlighting” below.

Untyped macros: reinterpret an expression

An untyped macro receives anything that parses as a Tauto expression as a syntax value, without type-checking it first. The standard library's nat! reinterprets == as propositional equality = and + as Nat::add, allowing theorem statements to look like mathematical expressions:

theorem add_comm_stmt(a: Nat, b: Nat): nat!(a + b == b + a) { Nat::add_comm(a, b) }

Because it runs before checking, it cannot inspect types. In return, it can accept expressions that would not otherwise type-check, such as an expression using == where that operator is not defined.

Typed macros: inspect types and context

A typed macro receives a checked expression as an opaque Judgement value containing its context, term, type, effect row, and variable usage. It runs only after the declaration containing the call has been checked once without macro expansion. User code never runs in the middle of type inference. This structurally rules out a cycle in which a macro inspects a type and then changes the type based on what it finds.

The output is accepted only if its type is definitionally equal to the original expression's type, its effect row is a subset of the original row , and the entire declaration passes checking again. Ownership, borrowing, and linearity are also checked across the whole expanded declaration. Matching types alone is not treated as a sufficient safety check.

If you also want to preserve meaning, you can choose the Proved result form, which returns a proof of equality e = e' alongside the transformation. The kernel checks that proof.

Tactics: macros that construct proofs

A macro taking ProofStep can be used inside a proof. The kernel checks the term it constructs against the explicitly written goal. Even if a tactic produces an incorrect proof, the kernel decides whether to accept it; the tactic itself does not need to be trusted.

Succ(k) => by rewrite!(Nat::add_comm(a, k)): Succ(Nat::add(a, k)) = Nat::add(Succ(k), a) {
  ⊢ Succ(Nat::add(k, a)) = Nat::add(Succ(k), a) from by rewrite!(Nat::add_succ_left(k, a)) {
    ⊢ Succ(Nat::add(k, a)) = Succ(Nat::add(k, a)) from Refl
  }
}

rewrite! is a standard-library tactic. Since the goal is written at every step, readers can follow the proof without knowing how the tactic is implemented.

Attribute macros: generate declarations

Writing @name!(…) before a declaration lets a macro generate declarations. This is a separate axis from the four kinds above: “attribute macro” describes the call's position, rather than a kind determined by its input type. The macro itself is a syntax macro or an untyped macro.

@mode!(`lookup(rec G, in i, out A) -> Looked { HasFound | HasNone }`) => inductive Looked, fn lookup
inductive Has: (List(Ty)) -> (Nat) -> (Ty) -> Prop { … }

This uses the standard library's mode! to turn the inductive relation below it into a decision function with uniquely determined outputs and a result type carrying a proof of correctness. It cannot transform arbitrary relations: the generator imposes conditions on the shapes of rules it accepts. The kernel checks the generated types and terms as usual.

The list after => names the declarations generated in addition to the original declaration, following the same listing rule. By default, the original declaration remains exactly as written. Rewriting it requires an explicit replace. A handwritten declaration cannot silently turn into something else.

Why list generated declarations?

A declaration-generating macro must list its generated declarations after => at every call. The macro already knows what it generates, so this could seem like something to infer automatically. Requiring it is deliberate: people and AI tools reading the source should be able to trace where a name came from without expanding the macro. Without the list, the origin of Looked or lookup would only become apparent after expansion. A mismatch between the list and the actual output is an error, so stale lists cannot remain unnoticed.

You do not, however, need to write the list by hand:

$ tauto fmt --fill-generated main.taut

This fills in missing or incorrect lists using the fixes suggested by the diagnostics. The completed list is written into the source, where readers can see it without expanding anything.

Hygiene: macros do not capture the caller's names

Identifiers carry both a name and a set of scopes. Each expansion adds and removes a fresh scope on its output. This gives the following behavior:

Identifiers introduced by a macro's quote do not capture the caller's variables.
Identifiers that came from the input resolve to the bindings intended by the caller.
Global names written in the macro refer to declarations in its definition file, even if the caller has declarations with the same names.
Intentional capture is possible only through an explicit operation, Syn::ident_like.

Captures are marked as such in tauto macro trace and are prohibited by lint in the standard library. The policy is to make hidden bindings visible.

Using effect analysis to contain macro execution

Macros execute arbitrary code at compile time. Rust procedural macros run with the compiler process's privileges, so they can access files and the network. Tauto restricts this through effect rows in the type system.

A macro function's effect row must be a subset of {macro_error, macro_warn, elab, Div}. A function with any other effect cannot be registered as a macro.

pub macro fn leak(p: swp::Pair): SynExpr ! {macro_error, Div} {
  let _ := read_file("/etc/passwd")
  quote { 1 }
}


FAILED macro: main.taut:2:10: macro.row: the function of a macro may perform macro_error, macro_warn, elab and Div, and `leak` performs fs_read

Reading a file performs fs_read, which is not allowed in a macro's row, so the macro is rejected. The same applies to networking, environment variables, the clock, randomness, and standard output.

Even if a standard effect were about to execute despite this check, the host running the macro would refuse to handle it and report an error. Directly calling built-in functions that access files or the network is rejected too.

What about infinite loops?

Div marks functions that may diverge. It is allowed in macros so they can use recursion and while, but macro execution is subject to budgets.

pub fn spin(n: i64): i64 ! {Div} { spin(n) }
pub macro fn loopy(p: swp::Pair): SynExpr ! {macro_error, Div} {
  let _ := spin(0)
  quote { 1 }
}


FAILED macro: main2.taut:2:10: macro.budget_exceeded: macro loopy took more than 10000000 steps

Budgets cover steps per call (10⁷ by default), the total per file (10⁸), expansion depth (64), output nodes (10⁵), and evaluator memory allocations (10⁷). Exceeding one produces a diagnostic and fails that declaration, while checking continues with the next declaration. Huge outputs and chains in which macros keep calling more macros are stopped in the same way. DSL strings are also limited to 1 MiB, and the parsing stack to a depth of 10⁴.

Macros also cannot:

Emit axiom, extern, or import, silently extending the set of things that must be trusted.
Create a hole such as ?h: syntax values have no constructor for holes.
Put include_text! into their output to read a file. Includes run before macro expansion, and only for calls explicitly written in the source.

Even a malicious macro from a dependency can only emit code that could be written by hand, within the allowed effects and execution budgets. Those effects include diagnostics. You can inspect its output with tauto macro expand, and the kernel ultimately checks it.

A powerful syntax-macro system

Write a grammar, get a typed AST and parser

A grammar passed to syntax! automatically produces a typed AST using struct and enum for its nonterminals, together with a parse function that is also usable at runtime. It can even be used directly as a syntax literal, without invoking a macro: math1 + 2 = 3 produces a math::Eqn value without running a macro.

The grammar notation is the same parol format used by tauto.par, which defines Tauto's own syntax. Users can therefore add their own languages using the same notation used for Tauto itself. Parsing is table-driven. The tables generated from a grammar are ordinary files that can be committed under .tauto-syntax/; the grammar generator does not have to run on every build.

Left recursion: LL(k) and LALR(1)

The default grammar class is LL(k), with lookahead k ≤ 3. Since left recursion is not allowed there, operators are expressed using repetition, such as { Plus Term }.

For more natural left recursion or operator precedence, specify %grammar_type 'LALR(1)' to generate an LALR(1) table:

syntax!(ex, ```

par
%start E
%grammar_type 'LALR(1)'
%%
E: E Plus T | T;
T: Num;
Num: /[0-9]+/;
Plus: '+';


```) => enum E, struct T

let r := ex`1 + 2 + 3`

The left-recursive production E: E Plus T works as written. Removing the %grammar_type line makes the grammar LL(k); lookahead conflicts then cause tauto syntax gen to reject it.

Both kinds of tables are generated by programs written in Tauto itself, in Nib: totes/llkgen and totes/lalrgen. The LALR(1) generator is written to construct the same states as lalry, the library used by parol, and tests compare their outputs. This is part of self-hosting Tauto's grammar infrastructure.

Ambiguous grammars are reported as conflicts. They are not accepted by retaining multiple parse results or hiding the ambiguity behind ordered choice. This keeps the typed AST unambiguous.

Syntax errors report locations and expectations

An error inside a DSL points to the actual line and column within the call's string and lists the terminals expected there:

2 + * 3 => error: macro.syntax_error: in calc: expected Num or LParen, found Star

For indented multiline literals, locations are adjusted for the indentation removed during parsing, so they still point to what the user wrote.

Registering formatters and syntax highlighting

syntax! accepts with(fmt: …, tokens: …) to attach functions that handle text in that syntax:

syntax!(layout, ```

par
%start Doc
%title "layout"
%%
Doc: Item { Comma Item };
Item: Num | Word;
Num: /[0-9]+/;
Word: /[a-z]+/;
Comma: ',';


```, with(fmt: layout_fmt, tokens: layout_tokens)) => struct Doc, struct Doc_Rep1, enum Item, fn parse

let d := layout`1,2 , foo,3`

When tauto fmt finds a literal in this syntax, it calls layout_fmt to format the contents:

let d := layout`1, 2, foo, 3`

layout_fmt and layout_tokens are ordinary Tauto functions that take a list of SynTok values (a token stream including whitespace and comments) or a lossless concrete syntax tree, SynCst. The ranges returned by tokens determine the language server's highlighting. Without a registered function, highlighting is inferred from terminal names.

The only effects these functions may have are Div and macro_error. They cannot access files or other external resources.

$name and ${…} inside a DSL are always highlighted as Tauto, whether or not tokens is registered. Any ranges returned by tokens that overlap these interpolations are trimmed. If the token function fails type checking, reports an error, or returns a range outside the text, the literal falls back to highlighting based on terminal names and gets a warning explaining why.

Formatters are also constrained. Before writing a result back, tauto fmt checks three things, keeping the original text and issuing a warning if any check fails:

The result parses as the same syntax.
The token sequence, excluding whitespace, is unchanged.
Formatting again leaves the result unchanged: the formatter is idempotent.

A formatter bug therefore cannot change tokens or leave the literal unparsable. These checks are not sufficient, however, for syntax where whitespace changes can change meaning, such as an indentation-sensitive grammar. Authors of fmt functions for such grammars still need to handle that carefully.

Embedding Tauto expressions in a grammar

The reserved terminal TautoExpr lets you embed a Tauto expression inside a DSL with ${ … }. The standard library's nat! uses this to embed Tauto expressions in mathematical notation:

pub theorem mul_comm(n: Nat, m: Nat): nat!(`$n * $m = $m * $n`) { … }

$n refers to the variable n, while ${Succ(k)} is an expression. Embedded expressions retain their actual source locations.

Build and prove a language implementation

In addition to the struct/enum AST, inductive_syntax! generates proof-side inductive types, with an ::I suffix such as Expr::I, and conversion functions such as Expr::to_i. You can then state theorems about the AST generated from the grammar.

examples/calc is a small language implementation that reads arithmetic expressions with addition and multiplication from text:

inductive_syntax!(arith, ```
{% endraw %}
par
%start Expr
%title "calc"
%%
Expr: Prod { Plus Prod };
Prod: Atom { Star Atom };
Atom: Num | Paren;
Paren: LParen Expr RParen;
Num: /[0-9]+/;
Plus: '+';
Star: '*';
LParen: '(';
RParen: ')';
{% raw %}

```) => enum Atom, struct Expr, … , fn parse, inductive Expr::I, … , fn Expr::to_i, …


$ tauto check examples/calc/proof/calc.taut
10 ok, 0 failed, 0 incomplete; 0 skipped, 124 from imports; axioms: none

Among the properties proved here is calc_run_correct: for any syntax tree, the compiled code runs without a stack underflow and leaves the value represented by that tree on the stack. The proofs check without additional axioms: axioms: none.

Some parts remain unproved. The text-to-tree parser arith::parse and the conversion to_i are outside these proofs. The parser is a driver over the tables produced by the grammar generator, and its correctness has not yet been formally established. There is no formal proof yet that the text has the meaning represented by the tree. What can currently be proved is soundness and completeness from the tree returned by the parser onward. Getting the AST as an inductive type makes it possible to start writing a proof of the parser itself; that proof is not complete.

More useful properties

Every expansion can be traced

Every node generated by a macro carries provenance: its call site, definition site, whether it was generated, and the chain of nested expansions. Diagnostics follow that chain to show which macro introduced what, for example: “x (introduced by expansion of math).”

tauto macro expand [--all | --at LINE:COL | --write | --json] FILE # inspect or write back the expansion
tauto macro trace [--json | --diff] FILE # trace expansion steps
tauto macro inspect FILE --at LINE:COL [--json]
tauto check --json # list expansions

With --write, you can write an expansion back to source and keep a version that no longer uses the macro. All these commands support --json, allowing AI agents to inspect macro expansion programmatically.

Typed macros do not change the declaration environment

Only syntax macros and attribute macros can generate declarations. A typed macro changes only the expression at its call site.

Write typing judgments in a DSL

In examples/lambda, theorems about typing and reduction in the simply typed lambda calculus can be written directly in the calculus's notation. A syntax named lc parses contextual judgments using a grammar containing |- and ~>*, and is also used inside proofs:

pub theorem k_star(): lc!(`(fun x: unit. fun y: unit. x) star ~>* fun y: unit. star`) { … }

Macro execution is ordered by file

You can only use macros defined in an earlier file or in a dependency tote (a package). Defining and using a macro in the same file is an error. This makes the timing of macro execution visible at a unit a reader can understand.

Deliberate restrictions

Here are the restrictions discussed above. These are freedoms found in some other macro systems that Tauto deliberately does not provide:

Access files, the network, environment variables, time, randomness, or standard output from a macro. Instead, include_text! reads a file only at an explicitly written call site.
Generate declarations or change the environment from a typed macro. Instead, syntax and attribute macros generate declarations, with the generated names listed in advance after =>.
Run a macro in the middle of type inference. Instead, a typed macro receives a checked expression as a Judgement.
Put axiom, extern, import, or a hole such as ?h in macro output. Instead, emit code that can be written by hand, subject to these output restrictions.
Silently replace a handwritten declaration. Instead, explicitly request replacement with replace.
Use a macro in the same file where it is defined. Instead, use a macro from an earlier file or a dependency tote.
Silently capture a variable. Instead, explicitly capture it with Syn::ident_like, leaving a trace.
Guarantee the output's type when the macro itself is written. Instead, check the expansion with the same checkers used for handwritten code.

Each of these freedoms can be useful. Tauto draws these boundaries to keep the trusted implementation small and expansions readable.

Design priorities

Soundness: do not accept invalid types, proofs, or authority.
Minimalism: minimize concepts, special rules, and trusted implementation.
Composability.
Expressiveness.
Security.
Readability for AI: machine-readable ASTs, types, errors, and expansion steps.
Performance.
Self-hosting.

What is not guaranteed

Proving the runtime evaluator correct is planned at the model level in Lean; correspondence with the Rust evaluator is checked by tests. A flaw in the evaluator could break macro isolation.
Macros are not prevented from generating code that performs dangerous actions. That code is treated the same way as the equivalent handwritten code, and can be inspected with tauto macro expand.
A macro close to a resource budget may succeed or fail differently after an evaluator version change. Usage above 90% of the limit produces a warning.
As noted above, the correctness of the grammar-generated parser remains unproved.
The language is still experimental. Syntax and diagnostic messages shown here may change.

Summary

Macros are ordinary functions returning syntax values. Their input types determine their kinds.
Expansions are checked by the same checkers as handwritten code, keeping macros out of the trusted base.
Hygiene uses scope sets. Capture requires an explicit operation and leaves a trace.
Effect rows prevent file and network access. Macros may use Div, but execution budgets turn nontermination into diagnostics.
Writing an LL(k) or LALR(1) grammar gives a syntax macro a typed AST, parser, and syntax literals. Formatters and highlighting can also be registered.
inductive_syntax! brings ASTs into the proof world, making it possible to state theorems about language implementations. The parser itself remains unproved.

Tauto on GitHub

Asynchronous Request and Connection Pooling in Elixir with Cizen

Ryo Hirayama — Sat, 20 Oct 2018 07:06:53 +0000

Introduction

Yesterday, I was really excited to write example Elixir codes with Cizen for this post. Cizen is a library to build applications with automata, events, (and fun!). With cizen, it becomes easier to create highly concurrent, monitorable, and extensible applications. I believe that Cizen has the potential to make our software development more fun as like Elixir does. In this post, we will build an API client which implements asynchronous request and connection pooling with Cizen.

Automata and Events

With using Cizen, we can use automata (plural of automaton) instead of processes. Automata communicate each other by subscribing and dispatching events in contrast with processes use direct messaging with pid.

API

In this article, we suppose that we need to get articles for each category from an API. The API works like the following:

get_category_id with a body "Elixir" (category name) returns a response with a body "01" (category ID)
get_articles with a body "01" (category ID) returns a response with a body ["Let's Try Elixir", "Implement an API with Elixir"] (list of articles)

Let's Get Ready

To get ready, run the following commands:

$ mix new client
$ cd articles

And add Cizen to dependencies:

# in mix.exs

  defp deps do
    [
      {:cizen, "~> 0.12.1"},
    ]
  end

Also, you need to prepare a simple mock of the API:

# in a new file request.exs

defmodule API do
  @categories %{
    "Elixir" => "01",
    "Nature" => "02",
    "Cizen" => "03"
  }

  @articles %{
    "01" => ["Let's Try Elixir", "Implement an API with Elixir"],
    "02" => ["Beautiful Nature"],
    "03" => ["Getting Started with Cizen", "Asynchronous Request with Cizen"]
  }

  def get_category_id(text) do
    :timer.sleep(:rand.uniform(10) * 50) # Delay for an API call
    @categories[text]
  end

  def get_articles(category) do
    :timer.sleep(:rand.uniform(10) * 50) # Delay for an API call
    @articles[category]
  end
end

Single Connection

Let's create Connection automaton. Connection automaton repeatedly receives Connection.Request event and dispatches Connection.Request.Reponse event for each request.

First, create Connection module and define those events:

# append the following to request.exs

defmodule Connection do
  defmodule Request do
    defstruct [:connection_id, :type, :body]

    use Cizen.Request
    defresponse Response, :request_id do
      defstruct [:request_id, :body]
    end
  end
end

use Cizen.Request makes Connection.Request requestive, and defresponse defines its response event.

Next, add the implementation of Connection automaton.

# append the following into Connection module

use Cizen.Automaton

defstruct []

alias Cizen.{Event, Filter}
alias Cizen.Effects.{Dispatch, Receive, Subscribe}

def spawn(id, %__MODULE__{}) do
  # Subscribe Connection.Request events for this connection.
  perform id, %Subscribe{
    event_filter: Filter.new(
      fn %Event{body: %Connection.Request{connection_id: value}} -> value == id end
    )
  }

  :loop
end

def yield(id, :loop) do
  request_event = perform id, %Receive{}
  %Request{type: type, body: body} = request_event.body

  # Calls the API
  response = apply(API, type, [body])

  perform id, %Dispatch{
    body: %Connection.Request.Response{
      request_id: request_event.id,
      body: response
    }
  }

  :loop
end

spawn/2 is called when the automaton is created, and yield/2 is called repeatedly until the automaton finishes. In yield/2, Connection handles Connection.Request and dispatches Connection.Request.Response one by one.

Now, we can use Connection to request to the API. Add the following code to run requests.

# append the following to request.exs

defmodule Main do
  use Cizen.Effectful

  def main do
    alias Cizen.Effects.{Request, Start}

    connection_id = handle fn id ->
      perform id, %Start{saga: %Connection{}}
    end

    ["Elixir", "Nature", "Cizen"]
    |> Enum.map(fn category ->
      fn ->
        handle fn id ->
          # Request to get a category ID
          response_event = perform id, %Request{body: %Connection.Request{
            connection_id: connection_id,
            type: :get_category_id,
            body: category
          }}
          %Connection.Request.Response{body: category_id} = response_event.body

          # Request to get articles
          response_event = perform id, %Request{body: %Connection.Request{
            connection_id: connection_id,
            type: :get_articles,
            body: category_id
          }}
          %Connection.Request.Response{body: articles} = response_event.body

          # Returns the articles
          articles
        end
      end
    end)
    |> Enum.map(&Task.async(&1))
    |> Enum.map(&Task.await(&1, :infinity))
    |> Enum.map(&IO.inspect(&1))
  end
end

# Run
Main.main()

Main.main/0 tries to get articles for three categories "Elixir", "Nature", and "Cizen", and the three processes are asynchronously run with using Task.async and Task.await.

Now, we can run request.exs with:

$ mix run request.exs

It outputs:

["Let's Try Elixir", "Implement an API with Elixir"]
["Beautiful Nature"]
["Getting Started with Cizen", "Asynchronous Request with Cizen"]

Request Logger

Before we use the connection pool, we should create a request logger to monitor the complex asynchronous requests.

Add RequestLogger:

# append the following above Main module in request.exs

defmodule RequestLogger do
  use Cizen.Automaton
  alias Cizen.{Event, Filter}
  alias Cizen.Effects.{All, Receive, Subscribe}
  alias Cizen.StartSaga

  defstruct []

  def spawn(id, %__MODULE__{}) do
    perform id, %All{effects: [
      %Subscribe{
        event_filter: Filter.new(
          fn %Event{body: %StartSaga{saga: %Connection{}}} -> true end
        )
      },
      %Subscribe{
        event_filter: Filter.new(
          fn %Event{body: %Connection.Request{}} -> true end
        )
      },
      %Subscribe{
        event_filter: Filter.new(
          fn %Event{body: %Connection.Request.Response{}} -> true end
        )
      },
    ]}

    %{
      connections: %{}, # connection ID => connection number
      requests: %{} # request ID => connection number
    }
  end

  defp tabs(n), do: Stream.cycle([" "]) |> Enum.take(20*n) |> Enum.join()
  def yield(id, state) do
    event = perform id, %Receive{}
    case event.body do
      %StartSaga{id: connection_id} ->
        put_in(state.connections[connection_id], Map.size(state.connections))
      %Connection.Request{connection_id: connection_id} = request ->
        connection_number = state.connections[connection_id]
        IO.puts("""
        #{tabs(connection_number)}request
        #{tabs(connection_number)}#{request.type}
        #{tabs(connection_number)}body: #{request.body}
        """)
        request_id = event.id
        put_in(state.requests[request_id], connection_number)
      %Connection.Request.Response{request_id: request_id} = response ->
        {connection_number, state} = pop_in(state.requests[request_id])
        IO.puts("""
        #{tabs(connection_number)}response
        #{tabs(connection_number)}#{inspect response.body}
        """)
        state
    end
  end
end

It looks a little bit difficult, but it simply logs Connection.Request event and Connection.Request.Response event to stdout. Also, it uses the horizontal axis for showing which connection is used and the vertical axis for the time sequence.

To use the logger, update Main.main/0;

Add perform id, %Start{saga: %RequestLogger{}} above the line starting the connection:

    connection_id = handle fn id ->
      perform id, %Start{saga: %RequestLogger{}} # here
      perform id, %Start{saga: %Connection{}}
    end

And, remove |> Enum.map(&IO.inspect(&1)) in order to avoid confusing with logging outputs:

    |> Enum.map(&Task.async(&1))
    |> Enum.map(&Task.await(&1, :infinity))
    # |> Enum.map(&IO.inspect(&1)) removed

Now, $ mix run request.exs outputs something like the following:

request
get_category_id
body: Nature

request
get_category_id
body: Cizen

request
get_category_id
body: Elixir

response
"02"

request
get_articles
body: 02

response
"03"

request
get_articles
body: 03

response
"01"

request
get_articles
body: 01

response
["Beautiful Nature"]

response
["Getting Started with Cizen", "Asynchronous Request with Cizen"]

response
["Let's Try Elixir", "Implement an API with Elixir"]

It shows that Connection.Request events are asynchronously dispatched, and the connection handles them in order. In the next section, we use multiple connections with connection pooling.

Connection Pooling

Now, let's create ConnectionPool automaton. It queues pushed connections and lends them with borrow event.

First, define Connection module and define related events:

# append the following above Main module in request.exs

defmodule ConnectionPool do
  defmodule BorrowConnection do
    defstruct []
    use Cizen.Request
    defresponse Lend, :borrow_id do
      defstruct [:borrow_id, :connection_id]
    end
  end

  defmodule PushConnection, do: defstruct [:connection_id]
end

ConnectionPool.BorrowConnection is a requestive event and ConnectionPool.BorrowConnection.Lend is its response event.

ConnectionPool.PushConnection is an event for registering a new connection or returning a borrowed connection.

Next, add implementation of ConnectionPool automaton.

# append the following into the ConnectionPool module

use Cizen.Automaton
alias Cizen.{Event, Filter}
defstruct []

alias Cizen.Effects.{All, Dispatch, Receive, Subscribe}

def spawn(id, %__MODULE__{}) do
  perform id, %All{effects: [
    %Subscribe{
      event_filter: Filter.new(fn %Event{body: %BorrowConnection{}} -> true end)
    },
    %Subscribe{
      event_filter: Filter.new(fn %Event{body: %PushConnection{}} -> true end)
    }
  ]}

  :loop
end

def yield(id, :loop) do
  borrow_event = perform id, %Receive{
    event_filter: Filter.new(fn %Event{body: %BorrowConnection{}} -> true end)
  }

  push_event = perform id, %Receive{
    event_filter: Filter.new(fn %Event{body: %PushConnection{}} -> true end)
  }
  %PushConnection{connection_id: connection_id} = push_event.body

  perform id, %Dispatch{
    body: %BorrowConnection.Lend{
      borrow_id: borrow_event.id,
      connection_id: connection_id
    }
  }

  :loop
end

Finally, update Main.main/0 to use multiple connections with ConnectionPool:

# replace Main.main/0 with the following

def main do
  alias Cizen.Effects.{Dispatch, Request, Start}

  handle fn id ->
    perform id, %Start{saga: %RequestLogger{}}
    perform id, %Start{saga: %ConnectionPool{}}
    # Starts 3 connections
    for _ <- 1..3 do
      connection_id = perform id, %Start{saga: %Connection{}}
      perform id, %Dispatch{
        body: %ConnectionPool.PushConnection{connection_id: connection_id}
      }
    end
  end

  ["Elixir", "Nature", "Cizen"]
  |> Enum.map(fn category ->
    fn ->
      handle fn id ->
        # Borrow a connection
        lend_event = perform id, %Request{body: %ConnectionPool.BorrowConnection{}}
        connection_id = lend_event.body.connection_id
        # Request
        response_event = perform id, %Request{body: %Connection.Request{
          connection_id: connection_id,
          type: :get_category_id,
          body: category
        }}
        %Connection.Request.Response{body: category_id} = response_event.body
        # Return the connection
        perform id, %Dispatch{
          body: %ConnectionPool.PushConnection{connection_id: connection_id}
        }

        # Borrow a connection
        lend_event = perform id, %Request{body: %ConnectionPool.BorrowConnection{}}
        connection_id = lend_event.body.connection_id
        # Request
        response_event = perform id, %Request{body: %Connection.Request{
          connection_id: connection_id,
          type: :get_articles,
          body: category_id
        }}
        %Connection.Request.Response{body: articles} = response_event.body
        # Return the connection
        perform id, %Dispatch{
          body: %ConnectionPool.PushConnection{connection_id: connection_id}
        }

        articles
      end
    end
  end)
  |> Enum.map(&Task.async(&1))
  |> Enum.map(&Task.await(&1))
end

Now, $ mix run request.exs outputs something like the following:

request
get_category_id
body: Cizen

                    request
                    get_category_id
                    body: Elixir

                                        request
                                        get_category_id
                                        body: Nature

response
"03"

request
get_articles
body: 03

                    response
                    "01"

                    request
                    get_articles
                    body: 01

                                        response
                                        "02"

                                        request
                                        get_articles
                                        body: 02

                                        response
                                        ["Beautiful Nature"]

                    response
                    ["Let's Try Elixir", "Implement an API with Elixir"]

response
["Getting Started with Cizen", "Asynchronous Request with Cizen"]

We made it! The requests are concurrently handled by the 3 connections.

Code Readability

I assume that you noticed that the above code of Main.main/0 is too complex, and it may be because we have two steps of perform/2 for starting a connection, and three steps for requesting. In such a situation Chain effect and Map effect will help us to make our code clear to understand.

First, add Main.start_connection/0:

# add the following into the Main module

defp start_connection do
  alias Cizen.Effects.{Chain, Dispatch, Start}
  %Chain{effects: [
    %Start{saga: %Connection{}},
    fn connection_id ->
      %Dispatch{
        body: %ConnectionPool.PushConnection{connection_id: connection_id}
      }
    end
  ]}
end

It joins the two effects, one for starting a connection and the other for dispatching ConnectionPool.PushConnection.

Next, add Main.request/2:

# add the following into the Main module

defp request(type, body) do
  alias Cizen.Effects.{Chain, Dispatch, Map, Request}
  effect = %Chain{effects: [
    %Request{body: %ConnectionPool.BorrowConnection{}},
    fn lend_event ->
      connection_id = lend_event.body.connection_id
      %Request{body: %Connection.Request{
        connection_id: connection_id,
        type: type,
        body: body
      }}
    end,
    fn lend_event, _ ->
      connection_id = lend_event.body.connection_id
      %Dispatch{
        body: %ConnectionPool.PushConnection{connection_id: connection_id}
      }
    end
  ]}
  %Map{
    effect: effect,
    transform: fn [_, response_event, _] -> response_event end
  }
end

It joins the three effects, one for borrowing a connection, another for requesting, and the other for returning the connection. After that, it also transforms the result so that perform id, request(type, body) will return the response for the request.

Finally, update Main.main/0 to use them.

# replace Main.main/0 with the following

def main do
  alias Cizen.Effects.Start

  handle fn id ->
    perform id, %Start{saga: %RequestLogger{}}
    perform id, %Start{saga: %ConnectionPool{}}
    # Starts 3 connections
    for _ <- 1..3 do
      perform id, start_connection()
    end
  end

  ["Elixir", "Nature", "Cizen"]
  |> Enum.map(fn category ->
    fn ->
      handle fn id ->
        response_event = perform id, request(:get_category_id, category)
        %Connection.Request.Response{body: category_id} = response_event.body

        response_event = perform id, request(:get_articles, category_id)
        %Connection.Request.Response{body: articles} = response_event.body

        articles
      end
    end
  end)
  |> Enum.map(&Task.async(&1))
  |> Enum.map(&Task.await(&1, :infinity))
end

Now, our code is more readable than the old one.

DEV Community: Ryo Hirayama

For Macro Lovers: Could Tauto Have the World's Most Powerful Macro System?

Macros are ordinary functions that return syntax values

Macro kinds and when to use them

Syntax macros: write in your own grammar

Untyped macros: reinterpret an expression

Typed macros: inspect types and context

Tactics: macros that construct proofs

Attribute macros: generate declarations

Why list generated declarations?

Hygiene: macros do not capture the caller's names

Using effect analysis to contain macro execution

What about infinite loops?

A powerful syntax-macro system

Write a grammar, get a typed AST and parser

Left recursion: LL(k) and LALR(1)

Syntax errors report locations and expectations

Registering formatters and syntax highlighting

Embedding Tauto expressions in a grammar

Build and prove a language implementation

More useful properties

Every expansion can be traced

Typed macros do not change the declaration environment

Write typing judgments in a DSL

Macro execution is ordered by file

Deliberate restrictions

Design priorities

What is not guaranteed

Summary

Asynchronous Request and Connection Pooling in Elixir with Cizen

Introduction

Automata and Events

API

Let's Get Ready

Single Connection

Request Logger

Connection Pooling

Code Readability

Links