Dependent Types and Compile Time Types

Question

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?

Answer 1

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.