|
Dependent types are types that depend on values, possibly runtime values. In C# types can only depend on other types when using generics: List<T> depends on T.
In C++ there is std::array<T, n> (array with length encoded in type), where n must be known in compile time. With full dependent types one can write generic types like std::array and use them with runtime parameters.
In dependently-typed languages there are two main types: Sigma (dependent pair) and Pi (dependent function).
Example of Sigma type in pseudo C#: (uint n, Array<int, n> a); // array of any size
Pi: Array<T, (n + 1)> push(Type T, uint n, Array<T, n> a, T x) { ... }
Array<int, 3> x = push(int, 2, [1, 2], 3); // [1, 2, 3]
Generic function f<T> is similar to a dependently typed one with `Type T` argument (requires first class types and many DT-langs have them). Values, on which types may depend, shouldn't be mutable, while C# function arguments are mutable.A bit larger example: void Console.WriteLine(string format, params object[] args);
Using dependent types you can transform `format` into a heterogeneous array type containing only arguments specified in the format string. WriteLine("{%int} {%bool}", ?); // ?'s type is an array with an int value and a boolean value.
A heterogeneous map may be implemented as a map T with keys mapped to types and another map where keys are mapped to the values of a corresponding type in T. Probably this is not a good representation, but it is a valid one. |
I know it's possible to have DT in C#, I think your literal of '3' in the above example is constructed using the successor function (well, its moral equivalent) at compile time, I just can't find the article I read and there's very little out there for DT in C# at all. And it's over my head until I sit down with a good example and work it through.
I could use some simple DT for list lengths in my project.