An Encoding of Interaction Nets in OCaml

TL;DR

The paper addresses encoding Lafont's typed interaction nets in OCaml to obtain compile-time correctness guarantees while exploring parallel reduction. It develops a GADT-based encoding that enforces arity, value types, and port polarity, eliminating runtime checks. Through implementations of agents, rules, and attributes, the approach achieves exhaustiveness and type safety for reductions, and benchmarks demonstrate potential parallelism in certain algorithms (e.g., Fibonacci) with Moonpool. The work showcases OCaml as a viable host for parallel interaction-net implementations and outlines avenues for library choices and language extensions to further integrate nets into practical workflows.

Abstract

Interaction nets constitute a visual programming language grounded in graph transformation. Owing to their distinctive properties, they inherently facilitate parallelism in the rewriting step. This paper showcases a simple and concise approach to encoding interaction nets within the programming language OCaml, emphasising correctness guarantees. To achieve this objective, we encode not only the interaction net primitives, but also Lafont's original type system.

Figures (10)

• Figure 1: Graphical notations for agents and rules
• Figure 2: Examples of typed agents
• Figure 3: Boolean agents
• Figure 4: Connection between auxiliary ports
• Figure 5: Rules for conjunction