Remix clone Hacker News

new | show | ask | jobs Github

	▲	ethanlipson 4 hours ago
		I'm talking about cases where the array size is not known at compile time. For example, say the user passes in a list of numbers as command line arguments. Then we have `argv: Vec<String, argc>` If I want to map these to ints, then I'd like a compile-time guarantee that the resulting array `nums: Vec<Int, argc>` is the same length as argv. Lean and Idris can do this, but AFAIK no commonly used languages can. But unlike general dependent types, these are not hard to wrap one's head around and would save a lot of frustration, in my experience.