Data.Name

Deterministic nominal identities with phantom namespace brands.

A name’s semantic identity is one integer, drawn from Control.Fresh’s monotonic counter, so a run’s names are a pure function of allocation order: same program, same names, on every backend and every machine. The source spelling travels beside the identity as a presentation hint and carries no meaning; renaming a binder’s hint changes what a diagnostic prints and nothing else.

The phantom space parameter brands a name with its namespace. A consumer declares one marker type per namespace (terms, types, modules) and the checker refuses to mix them: Name(TermSpace) and Name(TySpace) are distinct types with no conversion. The brand is compile-time only; every name is one integer at runtime.

This is nominal identity, not a substitution framework. Once binders and references carry unique identities, substitution compares names directly and can never capture a same-spelled inner binder; disambiguating suffixes become the pretty-printer’s concern alone. The equality and ordering instances are hand-written on the payload so the brand is never constrained: a marker type needs no instances to brand a name. Opt-in: not in Base.

Types

Name

newtype Name(space) = Name(Int)

A branded nominal identity: one integer, one phantom namespace.

Binder

type Binder(space) = Binder { name: Name(space), hint: String }

A binder: the identity the checker compares, and the source spelling diagnostics print. Equality, ordering, and display are written by hand below, on the identity alone: a derived structural pair would let the diagnostic hint decide whether two binders are the same.

Instances

eqName

instance eqName : Eq(Name(space))

ordName

instance ordName : Ord(Name(space))

showName

instance showName : Show(Name(space))

eqBinder

instance eqBinder : Eq(Binder(space))

ordBinder

instance ordBinder : Ord(Binder(space))

showBinder

instance showBinder : Show(Binder(space))

Functions and Values

name_id

name_id : forall a. (Data.Name.Name(a)) -> Int

The integer identity a name carries. Serialization and hashing commit to this and the surrounding schema, never to an address or a random seed.

fresh_binder

fresh_binder : forall a. (String) -> Data.Name.Binder(a) ! {Control.Fresh.Fresh}

Allocate a binder with a fresh deterministic identity and the given presentation hint.

run_fresh(\() -> [render_binder(fresh_binder("x")), render_binder(fresh_binder("x"))])

[x%0, x%1]

bound_name

bound_name : forall a. (Data.Name.Binder(a)) -> Data.Name.Name(a)

A reference to a binder: the branded name the checker compares.

render_binder

render_binder : forall a. (Data.Name.Binder(a)) -> String

Render a binder as its hint plus its identity, deterministic and unique by construction. A prettier printer may use the hint alone where no sibling shares the spelling.