Adi Shavit (5) [Avatar] Offline
#1
I am trying to grok dependent types, in general and in Idris in particular, and there's something that I find unclear.

In C++ (my native tongue smilie), templates can have non-type template parameters. The values of these parameters have to be specified at compile time, and it is then, at compile time, that the value-dependant types are defined/created/generated/declared.
It is not possible to generate a dependent-type with a run-time value.

Beyond, syntactic differences, how are Idris dependent types different from what C++ does (albeit with somewhat awkward and possibly convoluted syntax)? After all, the whole point of Idris's strong type system is to catch type errors at compile time, so obviously the runtime behavior is already after all the compile time checks have succeeded.

If I was to define a fixed size list, then `append` would return a list of a new type with the new incremented size specified as part of the type. In C++, you would need to know the actual types, i.e. the size of the list, at compile time. There is no way to call append() on the result of the previous append() call, a runtime-determined number of times, because there is no (obvious) way to specify the type of the object to hold the previous result at runtime. Calling it recursively would cause a compile-time stack explosion.

What can Idris do that is different?

I think this distinction would help in explaining the additional power of dependent-types over existing type systems.




Edwin Brady (65) [Avatar] Offline
#2
The distinction is that in Idris types are first class, so can contain (more or less) any expression that can appear anywhere else. I don't know in much detail how the C++ type checker works, but in Idris type level evaluation will only continue as long as values are known. You can see this at the REPL, for example:

Idris> \m : List Int => [1,2,3] ++ m
\m => 1 :: 2 :: 3 :: m : List Int -> List Int

Here, Idris has evaluated as far as knowing that the result starts with 1 :: 2 :: 3, but stopped evaluating ++ at 'm' because it knows nothing more about 'm'.

There is a slightly related question in the FAQ, which may also help: http://docs.idris-lang.org/en/latest/faq/faq.html#evaluation-at-the-repl-doesn-t-behave-as-i-expect-what-s-going-on
Adi Shavit (5) [Avatar] Offline
#3
I'm not sure if this answer helps me understand better.
From further reading, it seems that the key to DT is the run-time types (as opposed to having no explicit types at run-time).
I cross posted this question here.
If you read the (incomplete) comment thread, it seems to me that main difference beyond syntax and ease of use, is the ability to use run-time checks on types as easily as compile time checks. E.g. like a bounded integer type.
Does this make sense?

If I understand your example correctly, then there should be no real problem defining a C++ template function `f` taking a non-type 3-tuple value parameter (or 3 compile-time values) and returning a 4-tuple at runtime (for the sake of the example, a tuple can be considered as a List with a compile-time known size).

See working example here:

#include <iostream>
#include <tuple>

// 3-value version:
template <int A=1, int B=2, int C=3> 
auto f(int m)
{
    return std::make_tuple(A,B,C,m); // {A,B,C,m }; // From C++17
}

// single value version:
auto head = std::make_tuple(1,2,3);
template <decltype(head)& = head> 
auto ff(int m)
{
    return std::make_tuple(std::get<0>(head),std::get<1>(head),std::get<2>(head),m);
}


int main()
{
    {
        auto tup = f(4);
        std::cout << "A = " << std::get<0>(tup) << ", "
                  << "B = " << std::get<1>(tup) << ", "
                  << "C = " << std::get<2>(tup) << ", "
                  << "m = " << std::get<3>(tup) << "\n";
    }
    {
        auto tup = ff(4);
        std::cout << "A = " << std::get<0>(tup) << ", "
                  << "B = " << std::get<1>(tup) << ", "
                  << "C = " << std::get<2>(tup) << ", "
                  << "m = " << std::get<3>(tup) << "\n";
    }
}