prototype.md

Prototype Specification

This document specifies a minimal demo prototype for Splic, enough to compile a basic power function with a compile-time exponent.

Status: implemented. See bs/prototype_next.md for ongoing work.

Motivation

The goal is to verify that two-level type theory (2LTT) can work in practice for zkVM code generation. We want a minimal working example that demonstrates:

1. Meta-level computation (running at compile time)
2. Object-level code generation via quotations
3. Splicing computed code into the output

The power function is an ideal test case: it has a loop (requires object-level control flow), the exponent is known at compile time (enables significant optimization), and the result is demonstrably different from naive implementation.

Target Example

User-facing syntax

fn power(x: [[u64]], exp: u64) -> [[u64]] {
    match exp {
        0 => #(1),
        1 => x,
        exp => {
            let exp2: [[u64]] = #{
                let x2 = $(power(x, exp / 2));
                x2 * x2
            };
            let odd: u64 = exp & 1;
            match odd == 1 {
                0 => exp2,
                1 => #($(exp2) * $(x)),
            }
        }
    }
}

code fn pow5(x: u64) -> u64 {
    $(power(#(x), 5))
}

Expands to:

code fn pow5(x: u64) -> u64 {
    let x2 = x * x;
    let x4 = x2 * x2;
    let x5 = x4 * x;
    x5
}

Note how the recursive call to power with compile-time exponent 5 gets fully unrolled into straight-line code.

Compile-time Computation

Pre-compute a value at compile time, splice into object code:

fn sum_n(n: u64) -> u64 {
    match n {
        0 => 0,
        n => sum_n(n - 1) + n,
    }
}

code fn sum_to_five() -> u64 { $(sum_n(5)) }

Expands to:

code fn sum_to_five() -> u64 { 15 }

This pattern—meta-level computation spliced into object-level code—is the core use case for 2LTT.

Syntax Constructs

Quotations and Splices

• #(expr) — produces object-level code from a meta-level expression
• #{ stmts } — produces object-level code from a block (equivalent to #({ stmts }))
• $(expr) — splices a meta-level expression producing object-level code into surrounding object-level context
• ${ stmts } — block splice (equivalent to $( { stmts } ))
• [[T]] — type representing object-level code of type T (lifting)

The $ syntax mimics Rust macros, which should feel familiar. The # syntax is concise and extensible.

Functions

• fn foo() -> T — meta-level function (runs at compile time)
• code fn foo() -> T — object-level function (included in runtime binary)
• lam(x: T) => expr — lambda expression (meta-level only; annotations required)
• fn(_: T) -> U — function type (used in parameter/return type positions)

A fn with [[T]] parameters/return type manipulates code at compile time. A code fn defines a function that exists in the resulting binary. The code keyword explicitly marks object-level functions—this is temporary until phase polymorphism is better understood.

Higher-order meta functions work: a function can accept a code-transforming lambda and apply it at compile time:

fn repeat(f: fn(_: [[u64]]) -> [[u64]], n: u64, x: [[u64]]) -> [[u64]] {
    match n {
        0 => x,
        n => repeat(f, n - 1, f(x)),
    }
}

code fn square_twice(x: u64) -> u64 {
    $(repeat(lam(y: [[u64]]) => #($(y) * $(y)), 2, #(x)))
}

Expands to:

code fn square_twice(x: u64) -> u64 {
    (x * x) * (x * x)
}

Phase Context

Expressions are checked in either meta-level or object-level context:

• fn signatures use meta-level types (Type); code fn signatures use object-level types (VmType)
• Inside [[T]], the type T is in object-level context
• #(expr) switches from meta-level to object-level context
• $(expr) switches from object-level to meta-level context

Primitive Types

Type	Description
u0	Unit type
u1	Boolean
u8	8-bit unsigned
u16	16-bit unsigned
u32	32-bit unsigned
u64	64-bit unsigned

Primitive Operations

• Arithmetic: +, -, *, /
• Comparison: ==, !=, <, >, <=, >=
• Bitwise: !, &, |

Language Constructs

Let binding

let x = e1;
let x: T = e1;

Optional type annotation. Required when type cannot be inferred. No pattern matching in let for the prototype—just simple variable binding.

Note: Use let bindings generously inside splices to avoid duplicating computations. Without explicit lets, the same code may be generated multiple times.

Match

match e {
    pat => e,
    ...
}

Requirements:

• Exhaustive: must cover all cases or include a match-all (_, x)
• No nested matching for the prototype

Type System

Core representation is documented in more detail in (bs/prototype-core.md)[bs/prototype-core.md].

Universes

Two separate universes:

• Type — meta-level types
• VmType — object-level types

Both are type-in-type for now (no universe hierarchy). This simplifies the prototype significantly.

Type is itself a value that can be passed as a function argument, enabling polymorphism:

fn id(A: Type, x: A) -> A { x }
fn test() -> u64 { id(u64, 42) }

Lifting

• [[T]] — meta-level type representing object-level code of type T

Dependent Return Types

Return types can depend on runtime values or type arguments. The return type expression is evaluated at the call site once the argument values are known:

// Type-argument-dependent return
fn const_(A: Type, B: Type, a: A, b: B) -> A { a }

// Value-dependent return (scrutinee drives type selection)
fn get_value(b: u1) -> (match b { 0 => u0, 1 => u16 }) {
    match b {
        0 => 0,
        1 => 42,
    }
}

Definitional Equality

Quote and splice cancel each other out:

• Splicing a quoted expression yields the original expression
• Quoting a spliced code value yields the original code

These rules enable meta-level computation to "run" during staging, producing splice-free object code. See Kovács 2022 for the formal treatment.

Bidirectional Type Checking

The typechecker is syntax-directed with no unification or constraint solving:

• Checking mode: Expected type provided, verify term matches
• Inference mode: No expected type, synthesize type from term structure

Type annotations are required on function signatures, but the body can infer types for:

• Bound variables (from lambda/let context)
• Return types (from body)
• Application arguments (from function type)

No implicit arguments are supported—all arguments are explicit.

Type Annotations

Users write types on:

• Function parameters and return types
• Let-bound variables (optional if inferable)

The body expressions are inferred.

Rationale

• code keyword: Explicit marking avoids phase inference complexity until patterns become clear.
• No implicit arguments: Skips Agda-style unification with pruning, eta-expansion, flexible/rigid spines.
• Type-in-type: Simpler than cumulative universe hierarchy—just need Type and VmType.
• Bidirection without unification: Syntax-directed only, no constraint solving—enough for prototype.
• Separate universes: Makes stage explicit at type level, easier to reason about than per-value stages.

Implementation Omissions

The following are explicitly NOT included in the prototype:

• User-defined types / ADTs / product types
• Full dependent types (indexed types, dependent products); basic value- and type-argument-dependent return types are supported
• Object-level control flow constructs (while, loops, goto)
• Effects / effect handling
• Implicit parameters
• Phase polymorphism inference
• Elaborate error messages (basic errors only)

Future Considerations

These features may be added after the prototype validates the core approach:

• Full dependent types (indexed types, proofs)
• Type inference with unification
• Implicit arguments
• GADTs / pattern matching on types
• Object-level control flow (functional goto, structured)
• Closure-free object language (as per Kovács 2024)
• Kind-level polymorphism (generics without dedicated syntax)

References

• Kovács 2022: Staged Compilation with Two-Level Type Theory
• Kovács 2024: Closure-Free Functional Programming in a Two-Level Type Theory
• Splic concept: docs/CONCEPT.md
• Control flow tradeoffs: docs/bs/functional_goto.md