7 ms·

You can make C++ types that depend on constant values computed at compile-time, but this isn't the same as dependent types. In a hypothetical dependently-typed

You can make C++ types that depend on constant values computed at compile-time, but this isn't the same as dependent types. In a hypothetical dependently-typed C++, I would be able to do this: template <typename T, int N> struct vec { T data[N]; }; vec<T,n> repeat(int n, T const& x) {...} Note the run-time value n appearing in the return type of `repeat`. Because of this, repeat (if we could write it) has a dependent product type: the actual return type varies based on an argument's value.

saurik 8y ago
Is this really required by the definition of dependent types? I definitely agree that this is a difference with Idris (which can parameterize types over not just values but essentially program fragments due to its proof checker and unification semantics), but I was under the impression that this was not required to be considered dependent types.
- matt-noonan 8y ago
  Yes, you really need at least Pi types (dependent products, as above) or Sigma types (dependent pairs) to have dependent types. So you could get away with it in Python by munging a return type based on a parameter, but not C++ or most other statically typed languages! Unfortunately it seems like there is a lot of fog around this. Even the wikipedia page for dependent types botches the first example: "pairs of numbers where the second element is greater than the first" is just a normal type. A dependent type would be something like "pair<int,vec<T,n>>" where the n is supposed to equal the first element of the pair. The waters are muddied even further by the fact that you can reproduce many of the canonical examples for dependent types using other mechanisms, as you pointed out below for the vector-append operation! Edit: After complaining a bit about the Wikipedia page, it was pointed out that you can think of that example as a Sigma type. I contend it is not obvious unless you have already spent time thinking about dependent types, though.

saurik 8y ago

Is this really required by the definition of dependent types? I definitely agree that this is a difference with Idris (which can parameterize types over not just values but essentially program fragments due to its proof checker and unification semantics), but I was under the impression that this was not required to be considered dependent types.

matt-noonan 8y ago
Yes, you really need at least Pi types (dependent products, as above) or Sigma types (dependent pairs) to have dependent types. So you could get away with it in Python by munging a return type based on a parameter, but not C++ or most other statically typed languages! Unfortunately it seems like there is a lot of fog around this. Even the wikipedia page for dependent types botches the first example: "pairs of numbers where the second element is greater than the first" is just a normal type. A dependent type would be something like "pair<int,vec<T,n>>" where the n is supposed to equal the first element of the pair. The waters are muddied even further by the fact that you can reproduce many of the canonical examples for dependent types using other mechanisms, as you pointed out below for the vector-append operation! Edit: After complaining a bit about the Wikipedia page, it was pointed out that you can think of that example as a Sigma type. I contend it is not obvious unless you have already spent time thinking about dependent types, though.