<p>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.</p>

<p>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.</p>

<p>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!</p>

<p>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, <em>both</em> 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 <em>total</em> functions, which ensures that evaluation will terminate (albeit sometimes after a lengthy delay).</p>

<p>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.</p>

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

<p>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.</p>

<p>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 <em>separate</em> 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.</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2016-03-07T19:20:27.533Z
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?
Adi Shavit
CC BY-SA 3.0
2016-03-07T22:01:09.633Z
It's your choice if you want type checking in your program to have a run-time component or not; it's a mode of use rather than something baked into how the language works. But run-time type checks can play into the static analysis; you check the run-time safety once and end up having a new type that is from that point statically known to be safe. Having this flexibility to express things in similar ways and to tie the static and dynamic semantics together is very powerful.
Levi Pearson
CC BY-SA 3.0
2016-03-08T06:59:31.873Z
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?
Adi Shavit
CC BY-SA 3.0
2016-03-08T08:42:22.180Z
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.
Levi Pearson
CC BY-SA 3.0
2016-03-08T09:08:30.490Z
A more concrete example in Idris that explains how to do your example of something C++ can't would be using a dependently-typed pair to represent the type of a Vector read at run-time. In Idris, this is a type `(n : Nat ** Vect n a)` that holds the number of values, `n`, paired with the Vector of those values. So, a Vector of 3 numbers read at run-time could be represented as `(3 ** [1, 3, 5])`. The `3` value serves as evidence for the length of the Vector at the type level (its type is `Vect 3 Int`), since the evidence wasn't known at compile-time.
Levi Pearson
CC BY-SA 3.0
2016-03-08T10:22:20.517Z
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](http://en.cppreference.com/w/cpp/container/dynarray)?
Adi Shavit
CC BY-SA 3.0
2016-03-08T18:16:33.443Z
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.
Levi Pearson
CC BY-SA 3.0
2016-03-08T19:20:07.910Z
I see, so presumably e.g. for indexing, `dynarray` would have to to define some bounded integer (run-time constructed) _type_ for indexed access, and the user will have to "cast" a regular integral index to this run-time type (essentially construct it) and get the run-time cast to "pass" before a valid unchecked access is ensured to be correct. 
It's like doing the bounds check once, outside the access method scope and then, with safety ensured, continuing unchecked with confidence. And this type of run-time type value dependency percolates through all other methods as well (if/where needed).
Adi Shavit
CC BY-SA 3.0
2016-03-07T01:53:26.077Z
2016-03-07T01:53:26.077Z
Levi Pearson
<p>I am trying to grok dependent types, and there's something that I find unclear. </p>

<p>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. </p>

<p>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. </p>

<p>If I was to define the proverbial fixed-size list/vector type (where the list size is embedded in the type), then <code>append()</code> 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 <code>append()</code> on the result of the previous <code>append()</code> 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. </p>

<p>What does e.g. Idris do that is different?<br>
What extra power comes from dependent-types in languages that support them?<br>
Alternatively, what is C++ missing to be considered as a language that supports dependent-types?</p>

<dependent-type>
Dependent Types and Compile Time Types
Adi Shavit
# Dependent Types and Compile Time Types

(Asked by: username_0 on 2016-03-06)

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?

**Tags:** dependent-type


---

## 1 answers

### Answer by username_1 on 2016-03-07. Score: 16 | Accepted answer

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.

> **Comments:**
> **username_0**: 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?  
> **username_1**: It's your choice if you want type checking in your program to have a run-time component or not; it's a mode of use rather than something baked into how the language works. But run-time type checks can play into the static analysis; you check the run-time safety once and end up having a new type that is from that point statically known to be safe. Having this flexibility to express things in similar ways and to tie the static and dynamic semantics together is very powerful.  
> **username_0**: 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?  
> **username_1**: 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.  
> **username_1**: A more concrete example in Idris that explains how to do your example of something C++ can't would be using a dependently-typed pair to represent the type of a Vector read at run-time. In Idris, this is a type `(n : Nat ** Vect n a)` that holds the number of values, `n`, paired with the Vector of those values. So, a Vector of 3 numbers read at run-time could be represented as `(3 ** [1, 3, 5])`. The `3` value serves as evidence for the length of the Vector at the type level (its type is `Vect 3 Int`), since the evidence wasn't known at compile-time.  
> **username_0**: 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](http://en.cppreference.com/w/cpp/container/dynarray)?  
> **username_1**: 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.  
> **username_0**: I see, so presumably e.g. for indexing, `dynarray` would have to to define some bounded integer (run-time constructed) _type_ for indexed access, and the user will have to "cast" a regular integral index to this run-time type (essentially construct it) and get the run-time cast to "pass" before a valid unchecked access is ensured to be correct.  It's like doing the bounds check once, outside the access method scope and then, with safety ensured, continuing unchecked with confidence. And this type of run-time type value dependency percolates through all other methods as well (if/where needed).  

---

