It's nobody on here is talking about Rheinhardt's #2 point: The US is not spending enough on regulation. He specifically points out that regulators are underfunded and understaffed. In the US, this is often an active strategy by conservative politicians to undermine regulations, and portray the story that the regulations are bad, when in fact, the regulatory agencies are being intentionally preventing doing their jobs efficiently.
Peter Reinhardt is specifically talking about pumping massive amounts of a synthetic liquid into the ground.
The history of the 20th century is full of people insisting that some industrial product is perfectly safe to dump into the environment in massive amounts, and then it turns out years later that it's not safe at all. I can't imagine the process for injecting some new synthetic into the ground taking less than four years in any situation. It's going to take more time than that just to do basic studies.
The specific kinds of regulations he's arguing about have been written in blood and tumors, and they exist for good reasons.
> They need to be actually hit by the load to care. (BTW I can confirm,
> although quite violent, pigeons seemingly don't readily learn from
> this experience... They are really fucking stupid.)
That doesn't sound stupid to me. Rather it sounds like they're willing
to put with a lot of annoyance in order to get food.
It's not about the food. It's about a place to rest their fat bodies. Lacking the agility of every other bird, they prefer strictly horizontal branches of a certain diameter. There is plenty of other trees around. They could just realize the particular ones in front of my window mean getting shot with stuff. Honestly, they could alternatively just contain themselves and not literally shit my plants kaputt. We could coexist.
Do you commonly see other birds disfigured because they kept ignoring deterrents? No?! That's because pigeons are fucking stupid.
The advantage of dependent typing systems is that you can say that the arguments to a matrix multiplication function must have dimensions (m, i) and (i, n) and that result will have dimensions (m, n).
As others have said, this isn't a unique value proposition of dependent types, by all means dependent types provide a solution to this, but so do many other approaches.
You can do this in C++ & Rust, and I've done something similar in Typescript. The point of the comment you're replying to is kind of making the point that pitches for dependent types probably should give examples of something not already solved by other systems (not that you can't do this in DT). See:
> Yeah, this seems like matrixes might not be a great first example for explaining the value of dependent types.
In order to adopt DT, you need to pay a combined cost of productivity loss in terms of established tooling and choose to forgo any human capital which is no longer applicable once you start using a language with Dependent types, and a loss of time spent learning to use a language that has dependent types, which almost certainly has a smaller library ecosystem than most mainstream languages without DT.
For that reason it's worth considering what examples illustrate a benefit that outweighs all the above costs. I don't think it's enough to simply assert some moral basis on safety when clearly salaries for work done in unsafe languages are already considerably high.
Yeah, right now there isn't really any example of the value tradeoff being high enough that its overcome the barriers to adoption. Examples making the benefits more clear are helpful in being able to talk about dependent types in my opinion because most programmers (including myself beyond a fairly surface-level understanding, honestly) probably aren't familiar with them; once that's been established, I think it's a lot easier to talk about why the approach hasn't yet become mainstream.
For example, with the potential utility in having dependent types for list APIs, the barrier is that in practice, it's not always straightforward to be able to define your code in a way where you actually know the size of the list. If I read input from a user, I might be able to do an initial check that a list of items is non-empty as part of the constructor for the type, but what happens if I want to start popping off elements from it? In practice, this seems like it would either force you to go back to manually checking or only ever process things in a purely functional way to avoid defining behavior that vary based on state that isn't known. If you're willing to take this approach, having the compiler enforce it is great! You have to be willing to use this approach often enough for it to be worth picking a language with dependent types though, and in practice it doesn't seem likely that people would choose to even if they were more aware of the option.
> Examples making the benefits more clear are helpful in being able to talk about dependent types in my opinion because most programmers (including myself beyond a fairly surface-level understanding, honestly) probably aren't familiar with them
There's probably some truth in that (I'm probably in this camp as well), though I feel sometimes adoption of things like this can often be a communication problem, and the people who understand these technologies the most may struggle to identify what aspect of these technologies are valued more by the people they are trying to pitch them too.
Like they might even find those aspects boring and uninteresting because they are so deep into the technology, that they don't even think to emphasis them. Which feels like a similar story where a technology early to the party didn't take off until someone else came back to them later (like fat structs and data oritented design gaining some interest despite early versions of these ideas date back to Sketchpad (1963)).
> For example, with the potential utility in having dependent types for list APIs, the barrier is that in practice, it's not always straightforward to be able to define your code in a way where you actually know the size of the list
Yeah this example crossed my mind as well, it's not immediately clear how you deal with IO or data the result of inputs from the outside world. Although I have feeling this has to be a solved problem.
I guess more generally with API design, sometimes you don't really know the system you want to model yet so there's diminishing returns in being overly precise in how you model it if those things are subject to change. Not sure how substantive a concern this is when weighing up using dependent types, but it is something that crosses my mind as an outsider to all this dependent type stuff.
The io issue can be solved in 2 ways:
* by returning the pair of the list and it's length.
* having functions that convert between simply typed and dependently typed lists.
However the ergonomics could probably be improved.
The API design is a real real issue, which is why I think something more "gradual" would be best.
I haven’t entirely followed what you meant by a solution to IO, but I’m not to surprising to hear there’s a solution.
I guess the point I had in mind was, in making the case of dependent languages stuff like this may not be immediately apparent (I might be confusing the concept of total languages or programming which may not necessarily be coupled to dependent types).
> as an aside by IO I do mean anything not known at compile time (interrupts & user input, network responses, network requests [who API may change in a breaking way], database entries, etc)
Not for matrix multiplication, because there's no term-level chicanery to worry about; you just need phantom types for the two dimensions on your matrix type.
You can express a lot just carrying phantom types around and using basic pattern matching: in Rust I can express multiplication, concatenation of vectors to matrices, and inverses of square matrices, using phantom types.
But I can't say this, or anything remotely like it:
struct Matrix<M: u32, N: u32, T> {
dim: (M, N),
// imaginary dependently typed vectors
cells: Vec<M, Vec<N, T>>,
}
impl<M, N, T> Matrix<M, N, T> {
fn mul<O: u32>(&self, &other: Matrix<N, O, T>) -> Matrix<M, O, T> {
let cells: Vec<self.m, Vec<other.o, T>> = do_the_thing();
Matrix {
// any other values in dim, or a different type in cells, would be a type error
dim: (self.m, other.o),
cells
}
}
}
In other words, there's no dependent pair construction without dependent types. (Or at least dependent kinds and some tricks.)
Are M and N supposed to be type parameters in your example? If so, then you don't need to store them in the struct. And once you remove that (and switch from dynamically sized vectors to statically sized arrays) your example becomes perfectly representable in Rust and C++ without dependent types
You could use statically sized arrays, but if you can't have the static sizes of the arrays as your type parameters, but instead some arbitrary M and N, the size of your data structure isn't part of your type and you don't get the statically verified safety benefits. You also can't express M + N or anything of the sort.
Neither C++ nor Rust really hurt for expressivity, though.
Another point of view is that the IT department isn't meeting the users' needs, and that they're bypassing IT because they just want to get their work done.
When one government bet on solar power failed (Solyndra) the message from the right in the US was, "look what a waste it is for the government to invest in solar technology," instead of taking the appropriate lesson. That lesson was that we weren't spending enough backing solar companies.
China shoveled billions into developing solar manufacturing technologies, and as a result they figure out how to cheaply mass-produce solar cells. Solyndra failed because they couldn't compete against the resulting cheap solar cells.
But solar panels are undergoing involution in China while there is mass youth unemployment. Alot of these are zombie companies selling at a loss and propped by provincial debt.
You're measuring success only in with regards to how it might benefit you as a foreigner, but dosen't necessarily mean it was wholly successful for the China.
reply