Dependent Types

[Vengarioth]

Syntax proposal : Dependent Types

Summary

Types with terms applied to them.

Examples

A Vector type with type parameter T and term parameter N. N is used to determine the number of components this Vector has. A Vector<f32; 4> for instance is a Vector with 4 components (x, y, z, w), each of type f32.

struct Vector<T; N> {
    values: [T; N],
}

A more extensive example with implementation blocks and limits to types and type terms.

struct Vector<T, N>
    where T: Numeric,
    N <= 4
{
    values: [T; N],
}

impl operator * for Vector<T, 4> {
    #[native_impl] // <- compiler tries to substitute a native implementation instead
    fn mul(self, scalar: T) -> Self {
        // optional implementation
    }

    #[native_impl]
    fn mul(self, other: Self) -> Self {
        // optional implementation
    }

    #[native_impl]
    fn mul(self, other: Matrix<T; 4, 4>) -> Self {
        // optional implementation
    }
}

References

• wikipedia on dependend types