6

I've been reading about this thing called dependent types.

So for example imagine a function firstNPrimes(int n) which returns an array of length n. In other words the type it returned would be int[n]. (In normal programming languages without dependent types all we can say is it returns int[] where the type doesn't specify the array length.)

I'm not entirely sure how useful this is though. I suppose if you had a cross product (into which that first function could be sent as arguments):

int[3] Cross(int[3] A, int[3] B){..}

which only worked on 3 dimensional vectors then maybe the compiler could type check this and avoid pointer issues.

Are there any real practical uses of dependent types that would be useful in everyday programming? Or are they mainly just useful for abstract logic?

  • 5
    You ask like everyday programming isn’t abstract logic... – Telastyn Nov 17 at 21:55
  • @Telastyn true but I mean like, it's not trying to prove Fermat's Last Theorem using set theory. – zooby Nov 17 at 22:44
  • 2
    Isn't your example useful in game development? We use a lot of linear and vector algebra there. Sometimes a bit of calculus. – Theraot Nov 18 at 1:20
  • 1
    @zooby yes, although there is value in that for library authors. You could do a lot of 1D, 2D, 3D, and 4D in one swap, even if the final application will only use, say 3D. – Theraot Nov 18 at 4:22
  • 1
    You might be interested in the example of how to type tensors used in machine learning and other applications of linear algebra. A tensor is logically an array of arbitrarily many dimensions; making a type system flexible enough to check the correctness of code that does complex tensor manipulations is quite tricky. – Eric Lippert Nov 19 at 0:28
18

I think what you might be missing is the value you are depending on doesn't have to be a constant like 3. The length is often specified generically, so you may not know the exact length, but you can specify constraints on that length between your return values and different arguments.

There are a lot of functions that require n > 0, like head for example.

There are a lot of functions that take an index that must be within the size of the vector.

There are a lot of functions that take two vectors that must be the same size as each other, like a dot product for example.

Dependent typing allows you to verify all of these sorts of constraints at compile time, validating at the very edge of your system.

  • Hi thanks. No I didn't miss that. Imagine putting firstNPrimes(n) with type int[n] and putting it into the Cross product. That was my point. – zooby Nov 18 at 3:39
  • 1
    @zooby: Seems reasonable to me. You can still take advantage of the compile-time checks. – Robert Harvey Nov 18 at 3:50
6

I suppose if you had a cross product:

int[3] Cross(int[3] A, int[3] B){..}

which only worked on 3 dimensional vectors then maybe the compiler could type check this and avoid pointer issues.

Yes, a compiler could check that A and B are of the correct size in all places where Cross is used, if the size is part of the type system. It could be an error when it isn't. And if there are such cases when it cannot be checked, either an error or warning at language designer discretion.

Are there any real practical uses of dependent types that would be useful in everyday programming?

This is a feature that restricts what you can do. You cannot pass the wrong size of array into Cross. And that is a good thing. This feature can make the language easier to read, and harderd to get wrong.

Futhermore, it is great for automatic marshalling, because the size of the buffer needed to transfer information is part of the type system, you can declare it as part of the interface, and - if declared correctly - could save you some buffer overflow problems.

It also allows you to match database types in your code. For example, a string limited to a given number of characters.


Or are they mainly just useful for abstract logic?

A depedendent type is a type parametrized by values. It happens all the time in - drum roll - C++. You can create a template that has value parameters.

Here is a simple example:

template<int N>
struct S { int a[N]; };

This defines an array member of the size specified as template argument.

Example usage:

S<10> s; // s.a is an array of 10 int
s.a[9] = 4;

Example taken from cppreference.

This is how std::array works. std:array is a template that takes a type and a size. You can use make_array if you want the size infered. If you go read about std::array you will find it is less versatile than C-style arrays. As I was saying, this feature restrict what you can do. In exchange you gain static checking.

We could use C++ template system to define N dimensional vector algebra. And given that C++ support specialization, we could also handle operations not common to all numbers of dimensions. For example a cross product of two 2D vectors being a 2D vector does not make sense, but a wedge product of two 2D vectors which result is the length of the cross product of the two 2D vectors augmented with 0 in the third dimension does make sense.


For another example, I will turn to Ada. This is a subtype declaration in Ada:

subtype Count_To_Ten is Integer range 1 .. 10;

The above defines a type Count_To_Ten, all values of this type are also of type Integer, and are in the inclusive range from 1 to 10.

Then

subtype Ten_Characters is String (Count_to_Ten);

The above defines a type Ten_Characters, all values of this type are strings, and the idex of characters is a Count_to_Ten, thus is a 10 characters string.

This example is taken from Ada Programming/Type System.

We can define those 3D vectors in Ada:

type Axis is range 1 .. 3;
type Vector3 is array (Axis) of Integer;

Alright, not exactly like that, yet I found a Vector3 type defined in Ada in OpenGLAda – OpenGL binding for Ada (those use an enum for the index and let you specify the type of the elements as long as it has arithmetic operations). I'd say, yeah, this has practical use: video games.

  • Hmm... I didn't know about dependent types in C++. I'm not sure it's a full implementation like Ada. Maybe I'm wrong. – zooby Nov 18 at 3:42
  • @zooby I only have passing familiarity with Ada, I do not know how deep the dependent type rabbit hole goes. However, if it helps C++ case, I believe it is possible to capture an instance of a lambda as a parameter of a template in modern C++ (Iirc, you need C++14), I'll try to find a good example. The thing is, nobody calls it dependent types in C++. Addendum: Well, I apported something, I'll take as a win. – Theraot Nov 18 at 4:31
  • @zooby here is an example of a lambda as a template parameter in C++: stackoverflow.com/a/55520878/402022 (although it does not answer the question where it was posted). It requires C++17 where constexpr lambda expressions were added (I was wrong on it being C++14). – Theraot Nov 18 at 4:41
  • Interesting. It's the kind of thing you never thought you needed until it's there. – zooby Nov 18 at 4:48
  • 1
    I really would not call it "dependent types" in C++ until you can do std::cin >> n; std::array<int, n> array; (i.e., lift non-constant values into the type system). – Tavian Barnes Nov 18 at 15:53
6

Let's take a real-world example. Or better, real-mars.

NASA's Mars Climate Observer crashed into Mars because the software confused meters and feet. This was possible because the software treated all distances as just numbers. In physics, quantities have units associated with them. Feet and meters are different units, but both are used with lengths. Seconds and meters are different units for different quantities.

In C++, you can express this in the type system. And you can even use this to deduce derived quantities, such as speed, in meters per second (m∙s-1) and areas, in square meters (m2).

If NASA would have used this, it could have compared meters and feet. The compiler would have introduced the right scale factor when converting feet to meters.

  • 2
    how does this specifically relate to dependent types? – Nathan Hughes Nov 18 at 14:18
  • 1
    @NathanHughes: The type Z in Z operator*(X,Y) depends on the types X and Y following SI rules. Specifically, the physical types are implemented as 7-tuples following the 7 basic SI units, and the return type of the multiplication operation is calculated by adding the tuples. Hence area (m2) times length (m) gives a volume (m3). – MSalters Nov 18 at 14:18
  • 3
    @zooby: A type that depends on another type is a generic type, but normally if we're talking about languages with dependent types, we're looking at types that have some associated value whose algebraic manipulations are different than the algebraic manipulations of types. – Eric Lippert Nov 19 at 0:15
  • 1
    @MSalters: A nit-picky point, but the software confused pounds with newtons, not meters with feet. But you make a good point; languages exist where the type system would have made the problem evident immediately. It's interesting to compare how different languages implement this; if the subject interests you, consider checking out docs.microsoft.com/en-us/dotnet/fsharp/language-reference/… – Eric Lippert Nov 19 at 0:21
  • 3
    The standard definition of “dependently typed” is types can depend on values, i.e. λP in the lambda cube. What this answer describes, types depending on types, is already featured in Fω and in any Hindley-Milner type language, as well as in C++ like you say. Those are not considered dependently-typed languages. – leftaroundabout Nov 19 at 0:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.