Introduction to HWML

HWML is a hardware description language that lets you design digital circuits using dependent types. It combines the precision of formal verification with the practicality of modern HDLs.

What Makes HWML Different

HWML uses dependent types to catch errors at compile time that other HDLs only find during simulation or synthesis. The type system ensures that your circuits are correct by construction.

The language has two syntaxes. The surface language is what you write. The core language is the internal representation used by the compiler. This documentation focuses on the surface language unless you’re working on the compiler itself.

A Simple Example

Here’s a NOT gate in HWML.

prim Bit : Signal

def not_gate (x : Bit) : Bit :=
  match x with
  | 0 => 1
  | 1 => 0
  end

The type system verifies that this function always returns a bit when given a bit. Pattern matching ensures all cases are covered.

Where to Go Next

If you’re new to HWML, start with the getting started guide. If you want to see what the language can do, check out the surface syntax reference. If you’re working on the compiler, the internals section documents the core IR and type system.

Getting Started with HWML

This guide will help you write your first hardware circuit in HWML.

Your First Circuit

The simplest circuit is just a wire that passes a signal through unchanged.

prim Bit : Signal

def wire (x : Bit) : Bit := x

This defines a function called wire that takes a bit and returns it. The prim Bit : Signal line tells the compiler that Bit is a primitive signal type.

Building a NOT Gate

A NOT gate inverts its input. We can define it using pattern matching.

prim Bit : Signal

def not_gate (x : Bit) : Bit :=
  match x with
  | 0 => 1
  | 1 => 0
  end

The match expression checks the value of x. If it’s 0, the result is 1. If it’s 1, the result is 0.

Next Steps

Now that you’ve seen the basics, you can explore more features in the reference documentation.

HWML Language Features

This guide walks through the main features of HWML using working examples. Every code snippet here is typechecked by the compiler, so you can trust that the syntax is correct.

Basic Definitions

Most HWML programs start by defining values. The def keyword introduces a new definition.

prim Bit : Signal

def id (x : Bit) : Bit := x

Type annotations are optional when the compiler can infer them.

prim Bit : Signal

def zero : Bit := 0
def one := 1

Functions

Functions can take multiple parameters. You can write them with or without type annotations.

prim Bit : Signal

def and_gate (a : Bit) (b : Bit) : Bit := a
def or_gate a b := a

Lambda syntax works too.

prim Bit : Signal

def not_gate : Bit -> Bit := fun x => x
def xor_gate := fun a b => a

Primitives

The prim keyword declares external types and values that the compiler knows about but doesn’t define itself.

prim Bit : Signal

def bit_zero : Bit := 0
def bit_one : Bit := 1

Function Types

Function types use the arrow ->. HWML supports dependent types, where the return type can depend on the value of a parameter.

prim Bit : Signal

def identity_type := Bit -> Bit
def gate_type := Bit -> Bit -> Bit
def dependent_fn (x : Bit) : Bit -> Bit := fun y => y

Hardware Arrow

The fat arrow => distinguishes hardware module types from regular mathematical functions. This matters because hardware modules represent synthesizable circuits, not just computations.

prim Bit : Signal

def hw_identity_type := Bit => Bit
def hw_gate_type := Bit => Bit => Bit

Pattern Matching

Pattern matching uses the match keyword. Each branch starts with a pipe and ends with an arrow pointing to the result.

prim Bit : Signal

def not_bit (b : Bit) : Bit :=
  match b with
  | 0 => 1
  | 1 => 0
  end

Meta Definitions

Meta definitions run at compile time. They’re useful for generating code or computing types.

prim Bit : Signal

meta bit_type := Bit
meta make_identity (t : _) := fun (x : t) => x

Let Expressions

Local bindings use let ... in syntax. Each binding is visible in the expressions that follow.

prim Bit : Signal

def example (x : Bit) : Bit :=
  let y := x in
  let z := y in
  z

Application

Function application is just whitespace. Write the function followed by its arguments.

prim Bit : Signal

def identity (x : Bit) : Bit := x
def result := identity 0

def and_fn (a : Bit) (b : Bit) : Bit := a
def and_result := and_fn 0 1

Grouping

Parentheses control precedence and grouping.

prim Bit : Signal

def nested := (fun x => x) 0
def fn_type := (Bit -> Bit) -> Bit

Parameter Styles

You can mix typed and untyped parameters however you want.

prim Bit : Signal

def fn1 a b c := a
def fn2 (a : Bit) (b : Bit) (c : Bit) : Bit := a
def fn3 (a : Bit) b (c : Bit) := a

Examples

prim Bit : Signal

def id (x : Bit) : Bit := x

prim Bit : Signal

def compose (f : Bit -> Bit) (g : Bit -> Bit) (x : Bit) : Bit :=
  f (g x)

prim Bit : Signal

def const_zero : Bit := 0
def const_one : Bit := 1
def always_zero (x : Bit) : Bit := const_zero

Core Language Reference (hwmlc)

Version: 0.1.0 Audience: Compiler engineers, tooling developers, type theory implementers

This is the formal reference manual for the hwml Core IR. This is not a tutorial. If you’re learning hwml, start with the user guide.

Prerequisites: This reference assumes familiarity with:

• Dependent type theory and bidirectional typechecking
• Normalization by Evaluation (NbE)
• De Bruijn indices/levels
• Inductive families with parameters and indices

Table of Contents

1. Overview
2. Syntax Grammar
3. Type System
4. Evaluation Semantics
5. Global Declarations
6. Design Rationale

Overview

The hwml Core IR is a dependently-typed lambda calculus with:

• Predicative universe hierarchy: U0 : U1 : U2 : ...
• Dependent function types (Pi types): ∀(%x : A) -> B where B may depend on %x
• Lambda abstractions: \%x -> e with implicit typing
• Applications: f x (left-associative juxtaposition) or f[x, y, z] (bracket notation)
• Inductive type families with parameters (uniform) and indices (varying)
• Data constructors for canonical values
• Pattern matching via case trees (constructor-only, no wildcards)
• Propositional equality: Eq A x y with refl and transport
• Hardware types: ^A, ^s A, ^m A with separate universe hierarchy
• Signal types: Bit, 0, 1
• Module types: M -> N (hardware arrow), mod %x -> e (module abstraction)

Key Design Decisions

1. Bidirectional Typechecking: Explicit Synth (inference) and Check (validation) modes
2. Normalization by Evaluation (NbE): Conversion checking via semantic evaluation
3. Explicit Type Constructor Syntax: #[@Name ...] for types, [@Name ...] for data, @Name for constants
4. Constructor-Only Patterns: Case expressions match only on data constructors
5. Two-Phase Module Checking: Signatures added before validation, enabling full mutual recursion

Syntax Grammar

The Core IR has a concrete textual syntax mapping to Syntax<'db> in crates/hwml-core/src/syn/basic.rs.

Notation Conventions

• %x, %y, %z - De Bruijn indices (variables bound by lambda/pi/let)
• @Name - Global constant references
• #[@Name ...] - Type constructor applications
• [@Name ...] - Data constructor applications
• U0, U1, U2 - Universe levels
• ∀(%x : A) -> B - Dependent function type (Pi type)
• \%x -> e - Lambda abstraction
• f x - Application (left-associative)
• f[x, y, z] - Bracket application (explicit multi-arg)

Core Syntax Forms

Type System

The Core uses bidirectional typechecking with three main judgments:

1. Synthesis (Γ ⊢ e ⇒ T): Infer the type T of expression e
2. Checking (Γ ⊢ e ⇐ T): Validate that e has type T
3. Universe Checking (Γ ⊢ T : Un): Validate that T is a type in universe Un

Implementation: crates/hwml-core/src/check.rs

Universes

Syntax: U0, U1, U2, …

AST: Syntax::Universe(n)

Typing Rule (Synth):

─────────────────
Γ ⊢ Un ⇒ U(n+1)

Evaluation: eval(Un, env) = Value::Universe(n) (canonical form)

Design Note: Universes are predicative (no Type : Type). Each universe Un is a type in the next universe U(n+1). This prevents Russell’s paradox and ensures logical consistency.

Variables

Syntax: %0, %1, %2, … (De Bruijn indices)

AST: Syntax::Var(n)

Typing Rule (Synth):

Γ[n] = T
─────────────
Γ ⊢ %n ⇒ T

Evaluation: eval(%n, env) = env[n] (lookup in environment)

Failure Mode: Index n out of bounds (unbound variable)

Design Note: De Bruijn indices eliminate alpha-equivalence issues. Index %0 refers to the most recently bound variable, %1 to the second-most recent, etc.

Constants

Syntax: @Name

AST: Syntax::Const(id)

Typing Rule (Synth):

Σ(@Name) = T
──────────────
Γ ⊢ @Name ⇒ T

Evaluation: eval(@Name, env) = Σ(@Name).value (global definition lookup)

Failure Mode: Constant @Name not found in signature Σ

Design Note: Constants are global definitions with a fixed type and value. They are resolved by name during parsing and stored as ConstId in the AST.

Pi Types (Dependent Functions)

Syntax: ∀(%x : A) -> B or A -> B (non-dependent shorthand)

AST: Syntax::Pi(Option<String>, RcSyntax, RcSyntax)

Typing Rule (CheckType):

Γ ⊢ A : Un
Γ, %x : A ⊢ B : Um
──────────────────────────
Γ ⊢ (∀(%x : A) -> B) : Umax(n,m)

Evaluation: eval(∀(%x : A) -> B, env) = Value::Pi(name, eval(A, env), Closure(B, env))

Design Note: Pi types are the type of functions. The codomain B can depend on the value of the parameter %x. Non-dependent functions A -> B are syntactic sugar for ∀(%_ : A) -> B.

Lambda Abstractions

Syntax: \%x -> e

AST: Syntax::Lambda(Option<String>, RcSyntax)

Typing Rule (Check):

Expected type: ∀(%x : A) -> B
Γ, %x : A ⊢ e ⇐ B
──────────────────────────
Γ ⊢ (\%x -> e) ⇐ ∀(%x : A) -> B

Evaluation: eval(\%x -> e, env) = Value::Lambda(name, Closure(e, env)) (canonical form)

Failure Mode: Expected type is not a Pi type

Design Note: Lambdas are introduction forms for Pi types. They can only be checked, not synthesized (no type inference for lambdas).

Application

Syntax: f x (left-associative) or f[x, y, z] (bracket notation)

AST: Syntax::App(RcSyntax, RcSyntax)

Typing Rule (Synth):

Γ ⊢ f ⇒ ∀(%x : A) -> B
Γ ⊢ x ⇐ A
────────────────────────
Γ ⊢ f x ⇒ B[x/%x]

Evaluation:

• Beta reduction: eval((\%x -> e) v, env) = eval(e, env ++ [v])
• Neutral: eval(neutral v, env) = Value::Neutral(Eliminator::App(neutral, v))

Failure Modes:

• f does not synthesize to a Pi type
• x does not check against domain type A

Design Note: Application is the elimination form for Pi types. The result type B[x/%x] is the codomain with the parameter substituted by the argument.

Let Bindings

Syntax: let %x := e in body

AST: Syntax::Let(Option<String>, RcSyntax, RcSyntax)

Typing Rule (Synth):

Γ ⊢ e ⇒ A
Γ, %x : A ⊢ body ⇒ B
──────────────────────────
Γ ⊢ (let %x := e in body) ⇒ B

Evaluation: eval(let %x := e in body, env) = eval(body, env ++ [eval(e, env)]) (substitution)

Design Note: Let bindings are definitional (not recursive). The value e is evaluated and substituted into body. This is equivalent to (\%x -> body) e but more efficient.

Inductive Types

The Core IR supports inductive type families with parameters and indices.

Type Constructors

Syntax: #[@Name p1 p2 ... | i1 i2 ...]

AST: Syntax::TypeCon(TypeConId, Vec<RcSyntax>)

Typing Rule (CheckType):

Σ(@Name) = TypeConstructor { params: n, indices: m, universe: u }
Γ ⊢ p1 ⇐ P1, ..., Γ ⊢ pn ⇐ Pn
Γ ⊢ i1 ⇐ I1, ..., Γ ⊢ im ⇐ Im
────────────────────────────────────────
Γ ⊢ #[@Name p1 ... pn | i1 ... im] : Uu

Evaluation: eval(#[@Name ...], env) = Value::TypeCon(id, eval_args) (canonical form)

Design Note: Type constructors are type-level functions that produce types. Parameters are uniform across all constructors, while indices can vary per constructor.

Data Constructors

Syntax: [@Name a1 a2 ...]

AST: Syntax::DataCon(DataConId, Vec<RcSyntax>)

Typing Rule (Synth):

Σ(@Name) = DataConstructor { type_con: T, arg_types: [A1, ..., An], result_indices: [i1, ..., im] }
Γ ⊢ a1 ⇐ A1, ..., Γ ⊢ an ⇐ An
────────────────────────────────────────────────
Γ ⊢ [@Name a1 ... an] ⇒ #[T p1 ... pk | i1 ... im]

Evaluation: eval([@Name ...], env) = Value::Data(id, eval_args) (canonical form)

Design Note: Data constructors are introduction forms for inductive types. They produce values of the type constructor with specific indices.

Pattern Matching (Case)

Syntax: case e of { @Con1 %x %y -> branch1 | @Con2 %z -> branch2 | ... } : ReturnType

AST: Syntax::Case(RcSyntax, Vec<Branch>, RcSyntax)

Typing Rule (Synth):

Γ ⊢ e ⇒ #[@T p1 ... pk | i1 ... im]
For each constructor @Conj of @T:
  Γ, %x1 : A1, ..., %xn : An ⊢ branchj ⇐ ReturnType
Γ ⊢ ReturnType : Un
────────────────────────────────────────────────
Γ ⊢ (case e of { ... }) ⇒ ReturnType

Evaluation:

• Match: eval(case [@Con args] of { @Con %xs -> branch | ... }, env) = eval(branch, env ++ args)
• Stuck: eval(case neutral of { ... }, env) = Value::Neutral(Eliminator::Case(...))

Failure Modes:

• e does not synthesize to a type constructor
• Branches are not exhaustive (missing constructors)
• Branch patterns are not constructor-only (no wildcards)

Design Note: Case expressions are elimination forms for inductive types. They must be exhaustive (cover all constructors) and use constructor-only patterns (no wildcards or nested patterns).

Propositional Equality

The Core IR includes propositional equality as a primitive type former with reflection and transport.

Equality Types

Syntax: Eq A x y

AST: Syntax::Eq(RcSyntax, RcSyntax, RcSyntax)

Typing Rule (CheckType):

Γ ⊢ A : Un
Γ ⊢ x ⇐ A
Γ ⊢ y ⇐ A
──────────────────
Γ ⊢ Eq A x y : Un

Evaluation: eval(Eq A x y, env) = Value::Eq(eval(A, env), eval(x, env), eval(y, env))

Design Note: Equality types are heterogeneous in the sense that x and y must have the same type A, but A itself can be a dependent type. This is propositional equality (proof-relevant), not definitional equality (conversion checking).

Reflexivity (refl)

Syntax: refl

AST: Syntax::Refl

Typing Rule (Check):

Expected type: Eq A x y
Γ ⊢ x ≡ y : A  (conversion check)
──────────────────────────────
Γ ⊢ refl ⇐ Eq A x y

Evaluation: eval(refl, env) = Value::Refl (canonical form)

Failure Mode: x and y are not convertible (not definitionally equal)

Design Note: refl is the introduction form for equality types. It can only be used when x and y are definitionally equal (convertible via normalization).

Transport

Syntax: transport [%x] |- P proof value

AST: Syntax::Transport(Option<String>, RcSyntax, RcSyntax, RcSyntax)

Typing Rule (Synth):

Γ ⊢ proof ⇒ Eq A x y
Γ, %x : A ⊢ P : Un
Γ ⊢ value ⇐ P[x/%x]
────────────────────────────────
Γ ⊢ (transport [%x] |- P proof value) ⇒ P[y/%x]

Evaluation:

• With refl: eval(transport [%x] |- P refl value, env) = eval(value, env) (transport along refl is identity)
• Stuck: eval(transport [%x] |- P neutral value, env) = Value::Neutral(Eliminator::Transport(...)) (transport on neutral proof is stuck)

Failure Modes:

• proof does not synthesize to an Eq type
• value does not check against P[x/%x]
• Motive P is not a valid type family

Design Note: Transport is the elimination form for equality types. It allows converting a value of type P[x/%x] to type P[y/%x] given a proof of Eq A x y. This is the core mechanism for proof-relevant type casting.

Hardware Types

The Core IR includes a separate universe hierarchy for hardware description, enabling type-safe hardware synthesis.

Universe Hierarchy

Syntax: SignalUniverse, HardwareUniverse, ModuleUniverse

AST: Syntax::SignalUniverse, Syntax::HardwareUniverse, Syntax::ModuleUniverse

Typing Rules: These universes are not synthesizable. They can only appear as expected types in checking mode.

Design Note: Hardware types live in a separate universe hierarchy from computational types. This prevents mixing hardware and software types inappropriately.

Lift (^)

Syntax: ^A

AST: Syntax::Lift(RcSyntax)

Typing Rule (CheckType):

Γ ⊢ A : Un
──────────────────────────
Γ ⊢ ^A : HardwareUniverse

Evaluation: eval(^A, env) = Value::Lift(eval(A, env)) (canonical form)

Design Note: Lift converts a computational type A into a hardware type ^A. This represents synthesizable hardware that computes values of type A.

Hardware Arrow (->)

Syntax: M -> N

AST: Syntax::HardwareArrow(RcSyntax, RcSyntax)

Typing Rule (CheckType):

Γ ⊢ M : HardwareUniverse
Γ ⊢ N : HardwareUniverse
──────────────────────────
Γ ⊢ M -> N : ModuleUniverse

Evaluation: eval(M -> N, env) = Value::HardwareArrow(eval(M, env), eval(N, env)) (canonical form)

Design Note: Hardware arrows represent stateful hardware modules (sequential circuits) that transform input hardware to output hardware. Unlike Pi types, hardware arrows are non-dependent (the output type does not depend on the input value).

Module Abstraction (mod)

Syntax: mod %x -> e

AST: Syntax::Module(Option<String>, RcSyntax)

Typing Rule (Check):

Expected type: M -> N
Γ, %x : M ⊢ e ⇐ N
──────────────────────────
Γ ⊢ (mod %x -> e) ⇐ M -> N

Evaluation: eval(mod %x -> e, env) = Value::Module(name, Closure(e, env)) (canonical form)

Design Note: Module abstractions are the introduction form for hardware arrows. They represent sequential circuits with state.

Hardware Application (f<T>(x))

Syntax: f<T>(x)

AST: Syntax::HApplication(RcSyntax, RcSyntax, RcSyntax)

Typing Rule (Synth):

Γ ⊢ f ⇒ M -> N
Γ ⊢ x ⇐ M
────────────────────────
Γ ⊢ f<T>(x) ⇒ N

Evaluation:

• Beta reduction: eval((mod %x -> e)<T>(v), env) = eval(e, env ++ [v])
• Neutral: eval(neutral<T>(v), env) = Value::Neutral(Eliminator::HApp(neutral, T, v))

Design Note: Hardware application is the elimination form for hardware arrows. The <T> syntax allows explicit type arguments for generic modules.

Global Declarations

The Core IR supports three kinds of global declarations: type constructors, constants, and primitives.

Type Constructor Declarations

Syntax: tcon @Name (params: n) (indices: m) : Uu

Purpose: Declare an inductive type family with parameters and indices.

Example:

tcon @Vec (params: 1) (indices: 1) : U0

This declares a vector type Vec A n where A is a parameter (the element type) and n is an index (the length).

Data Constructor Declarations

Syntax: dcon @Name : TypeSignature

Purpose: Declare a constructor for an inductive type.

Example:

dcon @Nil : ∀(A : U0) -> #[@Vec A | @Zero]
dcon @Cons : ∀(A : U0) -> ∀(n : @Nat) -> A -> #[@Vec A | n] -> #[@Vec A | @Succ n]

Constant Declarations

Syntax: const @Name : Type := value

Purpose: Declare a global definition with a type and value.

Example:

const @identity : ∀(A : U0) -> A -> A := \A -> \x -> x

Primitive Declarations

Syntax: prim @Name : Type

Purpose: Declare an external primitive with a type but no definition.

Example:

prim @Bit : SignalUniverse

Design Rationale

Why Bidirectional Typechecking?

Bidirectional typechecking separates synthesis (type inference) from checking (type validation). This makes the type system more predictable and easier to implement. Lambdas and case expressions can only be checked, not synthesized, which avoids complex type inference algorithms.

Why De Bruijn Indices?

De Bruijn indices eliminate alpha-equivalence issues (renaming bound variables). This simplifies substitution, conversion checking, and normalization. The downside is that indices are less readable than names, but the Core IR is not meant to be written by hand.

Why Constructor-Only Patterns?

Constructor-only patterns (no wildcards or nested patterns) simplify the type system and make exhaustiveness checking trivial. Wildcards and nested patterns can be desugared in the surface language.

Why Separate Hardware Universes?

Separating hardware types from computational types prevents mixing synthesizable and non-synthesizable code. This ensures that hardware modules can be compiled to Verilog without runtime dependencies.

Why Propositional Equality?

Propositional equality (proof-relevant) allows reasoning about equality at the type level. This enables dependent types to express invariants like “this vector has length n” or “this circuit has width w”. Definitional equality (conversion checking) is used for type checking, while propositional equality is used for proofs.