4 ms·

Eli5 dependent types? Chatgpt: Dependent types are a concept in computer science and programming languages where the type of a variable can depend on the valu

Eli5 dependent types? Chatgpt: Dependent types are a concept in computer science and programming languages where the type of a variable can depend on the value of another variable. In simpler terms, imagine you have a list of numbers and you also have information about how long that list is. With dependent types, you could create a type for the list that explicitly includes its length, ensuring at compile time that operations respect this length. This makes it possible to catch certain kinds of errors before the code even runs. For example, in a language with dependent types, you could specify a function to take a list of length 3 and no other sizes. If you tried to pass a list of length 4, the program wouldn't compile, preventing this kind of mistake early on. It's a bit like having an extra layer of safety checks, where the types are more expressive and can encode more intricate relationships between variables.

turndown 3y ago
It’s simplest explanation is that dependent types are types whose exact type use some kind of parameterized value in the definition. So a dependently typed array would use a parameterized length value as part of it’s definition(this is usually the easiest example to understand). So an array of length 4(of whatever type) could be identified as different from an array of length 5, etc.
icen 3y ago
Another classic use case is that you can have expressions in the types of your function, for example this won't compile: stringOrInt : (x : boolean) -> int -> (if x then String else int) stringOrInt true x = toString x stringOrInt false x = x + 1 1 + stringOrInt true 37 # this will error, because it knows you've not returned an int The other example that you can do in depedently typed languages, but is too involved to write out here, is make a type-safe printf, where the format string produces the types for the other arguments.
howenterprisey 3y ago
I never care much for chatgpt answers. I don't know why people post them on here. In the first sentence, "another" is wrong because you don't need two variables, you just need one. Final paragraph's wrong for the same reason. The example given is poor given that I can write [i8; 3] or int[3] in Rust or C and those very much do not have "dependent types" in the popular sense (Rust's const generics excepted). To be fair, those examples are technically dependent types, but it would be better to give an example that's impossible in those languages, such as "array with length at most 3" or "even integer". Finally, to nitpick, "a bit like" is unneeded hedging. Stack Overflow did a much better job: https://stackoverflow.com/questions/9338709/what-is-dependent-typing https://stackoverflow.com/questions/9338709/what-is-dependen.... Wikipedia's article is pretty bad and maybe I'll get around to fixing it at some point.
- ChadNauseam 3y ago
  I like ChatGPT’s answer better than yours. Rust’s cost generics and C++ aren’t dependent types in any sense. And saying “the type of one variable can depend on the value of another” is vague but a good intuition pump. Since I guess we’re doing dependent types explanations I’ll give it a go. Dependent types extend a type system with two new type thingies: 2-tuples where the type of the second element depends on the value of the first, and functions where the type of the function’s return value depends on the value that was passed to it.
  - howenterprisey 3y ago
    Ha! Looks like I was wrong and confusing refinement types with dependent types: https://cs.stackexchange.com/a/21733 https://cs.stackexchange.com/a/21733 (unless of course this person is also confidently wrong, heh) > Dependent types are types which depend on values in any way. A classic example is "the type of vectors of length n", where n is a value. Refinement types, as you say in the question, consist of all values of a given type which satisfy a given predicate. E.g. the type of positive numbers. These concepts aren't particularly related (that I know of). Of course, you can also reasonably have dependent refinement types, like "type of all numbers greater than n".
- mettamage 3y ago
  Because I had the question and I figured this was quicker. I didn’t know what dependent types were. So now you know why I do it. Also, I believe this is my first time doing it. I might be wrong. Is it better to ask and wait for an answer instead? There is nothing in the guidelines on HN about it. I don’t know what’s reasonable and I haven’t seen strong cultural norms from HN yet. I at least labeled that the text was from chatgpt as to not confuse it was my own text.
  - kccqzy 3y ago
    Did you forget about search engines that enable you to do your own research rather than asking a human or an LLM?

turndown 3y ago

It’s simplest explanation is that dependent types are types whose exact type use some kind of parameterized value in the definition. So a dependently typed array would use a parameterized length value as part of it’s definition(this is usually the easiest example to understand). So an array of length 4(of whatever type) could be identified as different from an array of length 5, etc.

icen 3y ago

Another classic use case is that you can have expressions in the types of your function, for example this won't compile: stringOrInt : (x : boolean) -> int -> (if x then String else int) stringOrInt true x = toString x stringOrInt false x = x + 1 1 + stringOrInt true 37 # this will error, because it knows you've not returned an int The other example that you can do in depedently typed languages, but is too involved to write out here, is make a type-safe printf, where the format string produces the types for the other arguments.

howenterprisey 3y ago

I never care much for chatgpt answers. I don't know why people post them on here. In the first sentence, "another" is wrong because you don't need two variables, you just need one. Final paragraph's wrong for the same reason. The example given is poor given that I can write [i8; 3] or int[3] in Rust or C and those very much do not have "dependent types" in the popular sense (Rust's const generics excepted). To be fair, those examples are technically dependent types, but it would be better to give an example that's impossible in those languages, such as "array with length at most 3" or "even integer". Finally, to nitpick, "a bit like" is unneeded hedging. Stack Overflow did a much better job: https://stackoverflow.com/questions/9338709/what-is-dependent-typing https://stackoverflow.com/questions/9338709/what-is-dependen.... Wikipedia's article is pretty bad and maybe I'll get around to fixing it at some point.

ChadNauseam 3y ago
I like ChatGPT’s answer better than yours. Rust’s cost generics and C++ aren’t dependent types in any sense. And saying “the type of one variable can depend on the value of another” is vague but a good intuition pump. Since I guess we’re doing dependent types explanations I’ll give it a go. Dependent types extend a type system with two new type thingies: 2-tuples where the type of the second element depends on the value of the first, and functions where the type of the function’s return value depends on the value that was passed to it.
- howenterprisey 3y ago
  Ha! Looks like I was wrong and confusing refinement types with dependent types: https://cs.stackexchange.com/a/21733 https://cs.stackexchange.com/a/21733 (unless of course this person is also confidently wrong, heh) > Dependent types are types which depend on values in any way. A classic example is "the type of vectors of length n", where n is a value. Refinement types, as you say in the question, consist of all values of a given type which satisfy a given predicate. E.g. the type of positive numbers. These concepts aren't particularly related (that I know of). Of course, you can also reasonably have dependent refinement types, like "type of all numbers greater than n".
mettamage 3y ago
Because I had the question and I figured this was quicker. I didn’t know what dependent types were. So now you know why I do it. Also, I believe this is my first time doing it. I might be wrong. Is it better to ask and wait for an answer instead? There is nothing in the guidelines on HN about it. I don’t know what’s reasonable and I haven’t seen strong cultural norms from HN yet. I at least labeled that the text was from chatgpt as to not confuse it was my own text.
- kccqzy 3y ago
  Did you forget about search engines that enable you to do your own research rather than asking a human or an LLM?