Types are nothing but sets of possible values. Dependent types are just types that are defined using other values, i.e. they use values of some type in their own definition. Correct me if I am wrong about this, but this is my understanding right now.
This means that dependent types could be checked just like any other type by the compiler, if its definition is a completely constant expression. Otherwise, if it was dependent on runtime values, the compiler would need to add run time assertions at the right places.
The problem with Foo::set
is that this assertion is missing. To ensure that the data of Foo
is indeed of type Ordf32
, any data that is written to it needs to be Ordf32
, which does not happen in Foo::set
. These kinds of assertions should be done by the compiler and should be implicit and optimized, however it should be obvious when a typed is dynamically checked like this, as this might be expensive when it cannot be optimized away.
Maybe I am missing something but I think all we need for dependent types (and thus more verifiable code) is a syntax to tell the compiler "Ensure that values of this type always satisfy these conditions"
, first at runtime, then at compile-time using const functions.
This is basically what a type system is doing already, I imagine, so basically this is just a change to make the type system more programmable.