News for hackers. Stuff that matters.
Re:Notes on Idris (2017) by saurik on Thursday June 07, 2018 @10:43PM (#17262174)
Technically (and truly), C++ has dependent types, as types can depend on values [edit: matt-noonan has corrected me and pointed out this is wrong, but I think most of this comment is still useful]. (I can't say much about D, but I would believe it does as well; I could also see them having "simplified" away a really critical piece, though.)

A prototypical concept you would expect to find in a dependently typed language is "the ability to have a function that concatenates to arrays of sizes X and Y and returns an array of size X+Y that can be safely verified against further functions that also require arrays given as arguments to have specific lengths".

C++ is a bit indirect in its semantics here, but you will note that most other languages with generic types cannot express this thought (using either real integers or simulating them with types, either of which can be done in C++).

One could easily imagine "filling out" C++ to allow compile time type argument manipulation of more value types without even stressing its model, and in fact that is exactly the direction the language has been going in with constexpr. Here is an article on how to build a compile-time printf using C++14.

http://blogs.microsoft.co.il/sasha/2015/01/29/compile-time-r...

The only real limitation in C++ is that these values have to be relatively "concrete": at some level there has to be a number that can be calculated, as you can only deal with values as you don't have the amazing ability to do unification of program fragments like you have access to in Idris (like, you'd like to be able to say "the length of this array is the same as the length of this runtime string", and then after a bunch of array manipulation claim that you return a string five characters longer than the input string). Again, though: this could be added to C++ without breaking its underlying model. And it definitely is not required by the concept of "dependent types" [edit: matt-noonan points out it is, in fact, required for a language to have "dependent types" :(.]

Re:Notes on Idris (2017) by matt-noonan on Thursday June 07, 2018 @11:26PM (#17262360)
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.
Re:Notes on Idris (2017) by saurik on Thursday June 07, 2018 @11:34PM (#17262380)
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.
Re:Notes on Idris (2017) by matt-noonan on Thursday June 07, 2018 @11:46PM (#17262430)
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.

Re:Notes on Idris (2017) by pjmlp on Friday June 08, 2018 @02:57AM (#17263214)
Which is why after so many years of playing with FP on the sidelines, I have come to realize C++ has become a good way to use those concepts, while keeping my CV relevant for the kind of work I do.

Sometimes it feels like a kludge, but then I get to enjoy the nice IDEs, libraries that it has.

If only C++ had proper pattern matching support.

Of course, it isn't the only language I play with.

Re:Notes on Idris (2017) by Yuuri on Friday June 08, 2018 @08:27AM (#17264627)
Also, in C++ template value parameters are strongly limited to integral types, whereas in dependent types you can use any.