Infinity Language

AST Specification as Inductive Constructions

The idea of Infinity Langauge came from the needs of unification and arranging different calculuses as an extensions to the core of the language with dependent types (or MLTT core). While been working on distributed systems, data storages and stream processing, the core two languages: pi calculus and stream calculus discovered to be connected and being driven by a language with quantifiers as a primitives.

Infinity is a dependently typed language for stream processing, distributed processing and text processing. We use Coq to prototype the standard library including the theories needed to be able to prove code invariants instead of testing them. Infinity is a source to source translator that lets you use different languages at runtime: Erlang, Rust, Clang, Futhark, Julia, etc.

Infinity language presents a solid and unified way of modeling inter-language computations and inter-system communications within a single language with compact core. We strive for utilizing parallel hardware such as GPU and SSE/AVX SIMD instructions and providing a robust and verified distributed environment with process and channels runtime.

Inf Language is built on top of CoC pure type system, predicative universes and inductive constructions you may find in other MLTT provers like Lean, Coq, Idris, Agda, and F*. As algebraїс prover, Inf supports data and record polynomial functors as fundamental language constructions implemented in a form of hygienic macros over the AST. Everything in Infinity Language is encoded as inductive construction: from the equality property up to process calculus. Both Infinity language and its macrosystem are built using AST types, described in this document.

Language Extensions

Require Import core. Require Import homotopy. Require Import pi. Require Import stream. Require Import effect. Inductive MLTT := Pi: MLTT -> MLTT -> MLTT | Lam: Binder -> MLTT -> MLTT | App: MLTT -> MLTT -> MLTT | Sigma: MLTT -> MLTT -> MLTT | Pair: MLTT -> MLTT -> MLTT | Fst: MLTT -> MLTT | Snd: MLTT -> MLTT | Where: MLTT -> Decls -> MLTT | Var: Ident -> MLTT | U: MLTT | Con: Label -> list MLTT -> MLTT | Split: Loc -> list Branch -> MLTT | Sum: Binder -> NamedSum -> MLTT | HIT: HomotopyCalculus -> MLTT | PI: PiCalculus -> MLTT | EFF: EffectCalculus -> MLTT | STREAM: StreamCalculus -> MLTT.

Compiler Passes

  1. INF — Macro Expansion
  2. NORMAL — Typechecking
  3. ERASE — Type Information Erasure
  4. EXTRACT — Extract VM Lambda

Calculus

The type system is completely described by the PTS SAR notation, given by Barendregt. Find more info in Axioms and Inference Rules of underlying Om intermediate language.

record PTS: * := (S: ∀ (n: nat) → star n) (A: ∀ (i: nat) → type i (succ i)) (R: ∀ (i: nat) → ∀ (j: nat) → pi i j (max i j))

Macrosystem

Om

Om language is the macrosystem terminal language. Language forms of pure Macro or inpure Effect types are expanded to the terminal language. For the details please refer to the Om Assembler description.

data Om: * := (star: Star → Om) (var: Var → Om) (app: App → Om) (arrow: Arrow → Om) (pi: Pi → Om)

Star

record Star: * := (index: nat)

Variable

record Var: * := (name: string)

Arrow / Pi

record Arrow Pi: * := (name: string) (arg: Om) (body: Om)

Application

record App: * := (fun: Om) (arg: Om)

Macro

Macro language subsystem is the core of Inf language and dedicated to compile the prelude desceibed in the Core Types document. Om language is the target language of macroexpansions of data and record inductive constructions, let construction and univariable case pattern matching.

data Macro: * := (record: Record → Macro) (data: Data → Macro) (let: Let → Macro) (case: Case → Macro)

Case / Receive

record Case Receive: * := (of: Inf) (legs: list (prod atom (prod Om Inf))) (default: Inf)

Let

record Let: * := (binds: list (prod string Inf)) (in: Inf)

Record / Data

record Record Data: * := (name: string) (base: Om) (body: list (prod string Inf))

Effect

Effect syntax extensions defined basic process calculus axioms, IO and exception handling.

data Effect: * := (receive: Receive → Effect) (spawn: Spawn → Effect) (send: Send → Effect) (try: Exception → Effect) (raise: Exception → Effect) (write: File → Effect) (read: File → Effect)

Process

record Process: (Sigma: *) → (X: *) → * := (action: Sigma → X → GenServer X)

Spawn

record Spawn: (proc: Process) (raise: list Eff)

Send

record Send: (Sigma: *) → * := (message: Sigma) (to: Process Sigma)

Resources

  1. Om archives.
  2. Inf archives.
  3. Git sources.
  4. Inf git sources.