4
About what they are statically typed languages I am already aware, but the concept of dependently typed language is new to me.
I think it has to do with something called dependent types, but I also don’t know what they are.
3
What are dependent types?
It is the type that depends on its value and not just the general qualification of what fits there.
The most typical example is the type that allows establishing a range of allowed values.
Functional languages end up using this implicitly since they do not usually have imperative flow control to make decisions under certain values, so the value influences polymorphism ad-hoc, this is a form of dependent type (or at least can be), but it does not enter the typing system.
Another common example are the algebraic types that have an internal type that depends on the main type, so an object value determines the second part of the type.
The most interesting thing is when you put in the type what it can accept (it is similar to generics, but it accepts an argument with value instead of just one type):
type BoundedInt(n) = {i : Int | i <= n}
Without the dependent types you would have to write the code that checks if it is within the established range everywhere that uses this type.
In theory they are the superssum of robustness. In practice they complicate the language in every sense, and few languages adopt, in general the functional ones adopt because they want more mathematical rigor. And that is why the languages they adopt tend to receive the impression that their codes after compilation are always right (except logic error). Sure, at the expense of a lot of headaches.
A dependently typed language is one that has a dependent type Feature? Or is there something else?
I believe we can classify it this way, just have this Feature, At least I don’t see anything different from that. Just understand that you don’t need all the typing to be dependent.
Every language with dependent types must necessarily be statically typed?
A dynamic typing language could have dependent types for values, but not for variables. So it doesn’t make much sense. Dependent types are used to give more robustness to applications, reinforce contracts more strictly, ie, it makes less sense to use in dynamic languages (maybe PHP adopts :P I could not miss this :D) who don’t care much for it and many don’t even have the syntax to express it properly. And it must take work to make it right in that kind of language.
Browser other questions tagged characteristic-language typing language-independent computer-science type-theory
You are not signed in. Login or sign up in order to post.