Sigil

Sigil Type System Specification

Version: 1.0.0 Last Updated: 2026-03-14

Overview

Sigil currently uses bidirectional type checking with:

  • algebraic data types
  • exact record types
  • map types
  • explicit top-level parametric polymorphism
  • effect annotations

Current Sigil does not implement:

  • borrow checking
  • ownership/lifetimes
  • Hindley-Milner let-polymorphism

This spec describes the implemented checker in the current repository.

Bidirectional Checking

Sigil alternates between:

  1. synthesis: infer a type from expression structure
  2. checking: verify an expression against an expected type

This matches Sigil’s explicit surface:

  • function parameter types are required
  • function return types are required
  • lambda parameter types are required
  • lambda return types are required

Local Bindings

Local l bindings are monomorphic.

Sigil does not perform Hindley-Milner let-generalization for locals. Polymorphism comes from explicitly generic top-level declarations.

Explicit Top-Level Polymorphism

Generic declarations are allowed at top level:

λidentity[T](x:T)=>T=x
λmapOption[T,U](fn:λ(T)=>U,opt:Option[T])=>Option[U]

Generic instantiation is driven by ordinary bidirectional typing.

Current Sigil does not include:

  • generic lambdas
  • explicit call-site type arguments like f[Int](x)

Core Type Forms

Primitive types:

  • Int
  • Float
  • Bool
  • String
  • Char
  • Unit
  • Never

Constructed types:

  • [T]
  • {K↦V}
  • λ(T1,T2,...)=>R
  • named ADTs and aliases

Project-Defined Named Types

In projects with sigil.json, project-defined named types live in src/types.lib.sigil and are referenced elsewhere with µ....

Example:

t BirthYear=Int where value>1800 and value<10000

t User={birthYear:BirthYear,name:String}
λtodoId(todo:µTodo)=>Int=todo.id

src/types.lib.sigil is types-only and may reference only §... and ¶... inside type definitions and constraints.

Algebraic Data Types

Examples:

t ConcurrentOutcome[T,E]=Aborted()|Failure(E)|Success(T)

t Option[T]=Some(T)|None()

t Result[T,E]=Ok(T)|Err(E)

t Color=Red()|Green()|Blue()

Imported constructors use fully qualified module syntax in expressions and patterns.

Records and Maps

Records and maps are distinct:

  • records are exact fixed-shape products using :
  • maps are dynamic keyed collections using ↦

Sigil currently has:

  • no row polymorphism
  • no width subtyping for records
  • no open records

If a field may be absent, the canonical representation is Option[T] inside an exact record.

Constrained Types

Named user-defined types may carry a pure where clause:

t BirthYear=Int where value>1800 and value<10000

t DateRange={end:Int,start:Int} where value.end≥value.start

Constraint rules:

  • only value is in scope
  • the constraint must typecheck to Bool
  • constraints are pure and world-independent
  • v1 uses constraints as richer type meaning, not automatic runtime validation
  • the checker currently rejects only obvious literal contradictions

Structural Equality

Type equality normalizes unconstrained aliases and unconstrained named product types before comparison.

That means:

  • unconstrained aliases compare structurally
  • unconstrained named product types compare structurally after normalization
  • constrained aliases and named product types remain distinct
  • sum types remain nominal

This is a checker invariant, not inference.

Effects

Sigil supports explicit effect annotations in function and test signatures.

Sigil ships with primitive effects:

  • Clock
  • Fs
  • Http
  • Log
  • Process
  • Random
  • Tcp
  • Timer

Projects may define reusable multi-effect aliases only in src/effects.lib.sigil. Aliases must expand to at least two primitive effects.

Example:

effect CliIo=!Fs!Log!Process

Examples:

e axios:{get:λ(String)=>!Http String}

e console:{log:λ(String)=>!Log Unit}

λfetch()=>!Http String=axios.get("https://example.com")

λmain()=>!Http!Log Unit={
  l _=(fetch():String);
  console.log("hello")
}

Effects are explicit surface syntax. The checker tracks them as part of the typed program and rejects callees or bodies whose required effects are not covered by the enclosing signature.

Canonical Typed Rules

Some canonical rules depend on typing information.

Current important example:

  • a pure local binding used exactly once is rejected and must be inlined

This rule is applied after type checking by the canonical validator.

What This Spec Does Not Claim

This document intentionally does not specify:

  • ownership semantics
  • borrow rules
  • inferred lifetimes
  • Algorithm W

Those are not part of the implemented Sigil type system in this repository.

View source on GitHub