7
$\begingroup$

I am trying to grok dependent types, and there's something that I find unclear.

In C++, 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 languages with dependent types like e.g. Idris different from what C++ does (albeit with somewhat awkward and possibly convoluted syntax)? After all, the whole point of their strong type systems is also to catch type errors at compile time, so obviously any runtime behavior is already after all the compile time checks have succeeded.

If I was to define the proverbial fixed-size list/vector type (where the list size is embedded in the type), then append() would return a (new) 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 (as in a loop), 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 does e.g. Idris do that is different?
What extra power comes from dependent-types in languages that support them?
Alternatively, what is C++ missing to be considered as a language that supports dependent-types?

$\endgroup$
15
$\begingroup$

A language can be thought of as having both a static semantics, which determines the compile-time analysis that occurs; and a dynamic semantics, which determines the execution-time behavior of programs.

In Standard ML, for example, the static semantics concerns a language of Modules and a language of Types. The semantics show how types are assigned to terms in the core language and then checked for consistency. The module static semantics describe how signatures and structures are matched, how functors transform one structure to another, etc.

This is a fairly rich and complex language that is evaluated solely at compile-time; once this occurs, almost all of the semantic objects involved are no longer relevant to the execution semantics of the program and can be forgotten. The semantics works over the same syntax as the dynamic semantics, but the static semantics is very different in character from the dynamic semantics!

In a language such as Idris, which is dependently typed, the character of evaluation of the static semantics and the dynamic semantics ends up having far greater overlap. Instead of the static semantics working over types and the dynamic semantics working over values, both semantics now encompass both types and values. This doesn't mean that there aren't differences in the character of the static and dynamic semantics, just that there is significant overlap and they both concern some of the same semantic objects. In particular, the static semantics is often restricted to total functions, which ensures that evaluation will terminate (albeit sometimes after a lengthy delay).

Some parts of programs in dependently-typed languages exist only to provide evidence in the static semantics that other parts of the program are indeed well-typed. Idris doesn't make any syntactic distinctions here, but ATS (a systems programming language with dynamic semantics similar to C, but with a dependent type system) syntactically distinguishes terms that exist only to provide proof of assertions made in types. Idris does, on the other hand, allow annotation of programmer intent that some terms be "erased", which will produce an error in the static semantics if that desire can't be met.

Now, with that out of the way, let's look at C++ templates:

Instead of dealing with polymorphism and dependency of types on values directly in the static semantics, C++ adds an extra untyped language of template expansion into the static semantics. Rather than deal with complex static semantics, extra code is generated that should be checkable simply via the simple core language static semantics.

Although this lets you deal with some of the same practical problems that can be solved with polymorphic and more general dependent types (polymorphism is just a different sort of dependency, one of terms depending on types) it's not actually part of the type system; it's just an extra layer in the static semantics separate from the type system. Furthermore, the only way any extra "stuff" generated by template expansion could be erased would be by the general "dead code elimination" portion of the compiler, which isn't even a well-defined part of the static C++ semantics.

Sometimes in a dependently-typed language, type parameters can't be erased at run-time, because they are relevant to the determination of the run-time semantics. In C++, you would have to carry an extra parameter as well; this might be a "length" parameter that would be part of a Vector type in a dependently-typed language. C++ lacks the ability to make such parameters implicit and to define code that automatically calculates on them and make appropriate consistency checks with them.

Dependently-typed languages give you the choice of how much effort you will put into static proof of the runtime-irrelevance of such parameters; with little effort you can let them carry over into the dynamic semantics and be run-time checked, but with more effort you may be able to supply a proof that the property asserted by the type term is never violated and thus erase the run-time representation entirely.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Are you saying that dependent-type languages also have a run-time component or that the static proof gives something extra that the static type semantics do not? Also, with regards to C++ it seems like what you describe is a compiler implementation issue, not necessarily a limitation or constraint on the type system semantics. I don't understand what deficiency C++ has in this context. Could you maybe give an example of what you mean? $\endgroup$ – Adi Shavit Mar 7 '16 at 19:20
  • 1
    $\begingroup$ I think I am beginning to understand, but your answer is too general (and requires some background I don't have) that I don't see that it actually answers my question directly: "what is C++ missing to be considered as a language that supports dependent-types?" or to rephrase, what would one need to add to C++ to make it dependently typed, and what would it be able to do then that it cannot do now? $\endgroup$ – Adi Shavit Mar 8 '16 at 6:59
  • 1
    $\begingroup$ Well, to put it as plainly as possible, what it is missing is an actual dependent type system. I'm not certain that C++ can't do anything now that it could do with a dependent type system, as the C++ template language is Turing-complete, but a dependent type system is something that is designed that way; types end up as first class citizens in the language. It actively supports computing and proving at compile time via a language based on sound logic. Doing this in C++ is convoluted and inefficient; it's not designed for it. $\endgroup$ – Levi Pearson Mar 8 '16 at 8:42
  • 1
    $\begingroup$ IIUC, 3 is a run-time value and thus could have been any other number as well, so how is this different than a fixed-size at construction C++ class like e.g. std::experimental::dynarray? $\endgroup$ – Adi Shavit Mar 8 '16 at 10:22
  • 1
    $\begingroup$ That piece may not be very different, but the way it would fit into the overall system of reasoning about bounds checks would likely be different. dynarray doesn't seem to provide any way to prove you've done a bounds check before indexing the array, while that would be straightforward to express in Idris by requiring the index to be a bounded type with the same bound as the length in the Vector type. Once you run the check and get the bounded type, you never have to do it again. Again, with enough effort, you may be able to verify whatever you like in C++, but not by design. $\endgroup$ – Levi Pearson Mar 8 '16 at 18:16

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.