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.
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.
Ha! Looks like I was wrong and confusing refinement types with dependent types: 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".
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.
It's of course fine to ask chatgpt. I also appreciate that you wrote that it was from chatgpt.
However, I wouldn't recommend posting the result here if you don't know if it's correct. Moreover, anyone can ask chatgpt themselves. It's better to wait for someone here to post an answer.
Yes, there's nothing in the guidelines, but they're (deliberately) not all-encompassing. Besides, I would hope it's part of basic Internet etiquette; just because we now have access to tools that generate plausible-sounding but not necessarily correct answers to questions doesn't mean we need to post what they create in the place of genuine answers.
> Besides, I would hope it's part of basic Internet etiquette
Yea that got lost on me. I think I view these things a bit differently than most on HN. I've noticed in general that the more I'm not at uni, the more my thinking has become heuristic and quick-ish. It used to be more thorough and in-depth. The trade-off of it being that such type of thinking is more time consuming but the answer is more comprehensive and/or accurate.
> Is it better to ask and wait for an answer instead?
No, around here it's better to say "So dependent types are pretty much $SOMETHING_COMPLETLY_WRONG ?" and wait for all the "corrections" (aka Cunningham's law someone linked to nearby).
I could use google but chatgpt wins on speed and asking on HN wins on vine. When someone asks me a question I am mostly quite enthusiastic in explaining it. You can’t get that as easily from a search engine.
I don't see anything wrong with GPT's answer other than pedantic quibbling. I just don't like it because I don't want to share this space with non-humans.
Cunningham's Law: Post something wrong online so you can get a correct answer.
Half the ChatGPT answers on here seem to be wrong in obvious ways or, worse, subtle but critical ways. When people post them they get downvoted, and other people chime in with "Why are you trusting a fabulist like ChatGPT instead of going to actual resources with definitions and explanations that aren't garbage? Here's what it actually is..."
That is really interesting. Whish there was some better name for that, as I feel like it isn't that descriptive. However their benefit seem really obvious, saying that something is an areay, or even an array of integers is barely half the picture if in reality it is a array of length 5 of even integers to loan from your example. I guess you would try to implement it in other languages creating objects?
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-dependen.... Wikipedia's article is pretty bad and maybe I'll get around to fixing it at some point.