Crate mononym

Mononym is a library for creating unique type-level names for each value in Rust. The core type Named<Name, T> represents a named value of type T with a unique type Name as its name. Mononym guarantees that there can be no two values with the same name. With that, the Name type serves as a unique representation of a Rust value at the type level.

Mononym enables the use of the design pattern Ghosts of Departed Proofs in Rust. It provides macros that simplify the definition of dependent pairs and proof objects in Rust. Although there is still limited support for a full dependently-typed programming in Rust, Mononym helps us move a small step toward that direction by making it possible to refer to values in types.

See docs::implementation for how mononym implements unique name generation in Rust.

Modules

docs

This is a rustdoc-only module providing in depth documentation on the library.

named

The main implementation for named data types.

proof

Macros

exists

Macro to define new named value coupled with proofs in the form of dependent pairs.

exists_single

proof

Macro to help define a new proof type.

proof_single

Structs

Life

Turns a lifetime 'name into a unique type Life<'name> with an invariant phantom lifetime. Life implements Name so that it can be turned into a unique impl Name.

Named

Represents a named value with a unique type-level name. monoym guarantees that there can never be two Rust values of the same type Named<N, T>. With that, the name type N can be used to uniquely identify the underlying value at the type level.

Seed

A unique seed type for generating new unique names. mononym guarantees that there can never be two seed value of the same type Seed<N> with the same name type N.

Traits

HasType

A marker trait that is used to mark a type-level name being bound to a Rust value of the given type T. This helps ensure that functions that are generic over type-level names are “well-typed”, with each name “having” their own type through HasType.

Name

A marker trait that is used to represent unique type in Rust. mononym guarantees that any two impl Name generated by the library are always considered distinct types by Rust.

Functions

with_seed

Provides the continuation closure with a unique Seed with a unique lifetime 'name and a unique name Life<'name>.