Crate mononym[−][src]
Expand description
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
This is a rustdoc-only module providing in depth documentation on the library.
The main implementation for named data types.
Macros
Macro to define new named value coupled with proofs in the form of dependent pairs.
Macro to help define a new proof type.
Structs
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
.
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.
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
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
.
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
Provides the continuation closure with a unique Seed
with a unique lifetime
'name
and a unique name Life<'name>
.