Module rust_examples::dependent[−][src]

Expand description

This module includes Rust’s approach to dependent types.

Informally, a dependent type is a type that depends of a value of (or a term from) another type.

This example if from a talk (not only) about dependent types (~ 15:50 min): Proof Theory Impressionism: Blurring the Curry-Howard Line

More generally, according to the article Why dependent types matter:

Dependently typed programs are, by their nature, proof carrying code.

Finally, example of an HList is taken from hlist-rs.

Structs

Structure representing a non-empty HList consisting of a head and tail.

Structure representing the null pointer at the end of each HList.

Negative compilation tests for AddEq relation.

Negative compilation tests for Pred relation.

Type-level definition of a successor of a natural number N, i.e. the number N + 1.

A wrapper for Vec<A> which preserves the information about its size N at the type level (i.e. compilation time).

Type-level definition of the natural number 0.

Relation M: AddEq<N, X> is interpreted as M + N = X.

Trait representing a heterogeneous list, a.k.a HList of length N.

Trait representing a type-level definition of natural numbers (Peano numbers).

Trait encoding a predecessor relation: “Self is a predecessor of N”.