Comment by malcolmgreaves | Hacker News Reader

Comment by malcolmgreaves | Hacker News Reader

Parent Full thread

I'm glad you brought up languages that use dependent typing! And sure, static typing is just one tool of many: so it's not going to be the end-all-be all in the quest to answer the eternal question: "does my program work the way I think it does?" More refined, my claim is that it is a super powerful tool that brings substantial benefits. And that it's a mistake to not use this tool.

No tool is perfect. There will always be room for improvement as we use our current crop of tools, observe how they serve our needs and don't serve them, then use that knowledge to build even better tools.

> No language in common use today asserts anything beyond the most basic properties of a program using types. Idris and Coq do that, but they are extremely obscure even compared to Haskell or OCaml.

With enough time, we'll see the influence of dependent typing crop up in more common languages. For instance, there's the Rust crate dfdx, which uses dependent typing to encode the shapes of tensors. [1]

> It's also important to note that types are quite rarely used outside formal computer science.

This isn't quite right. At least, I think what you're saying is that "physics proofs don't set up typing rules therefore they don't use types." But then again, proofs aren't necessarily programs. Is every physics proof computable? I'm not a physicist so I'll defer that to an expert. My understanding is that physicists aren't interested in computability when they're communicating their ideas about the universe. For the subset of proofs that are computable, I'll make the argument that there exist types on the mathematical structures and operations on them that they're defining. These types needn't be written type and formalized with typing rules to exist.

[1] https://docs.rs/dfdx/latest/dfdx/

Physics has a simple form of types, namely units. Checking units at the end of solving a problem was emphasized by every physics professor I ever had.

As for dependent types, they're only one of the ways to express mathematical properties of programs. Check out what Ada/spark does for example. A layer of logic on top of a program doesn't have to be embedded in the types (and if your language is imperative you probably don't want that anyway).

Measurement units are not types. They are conceptually similar, but the way they are used is actually entirely different. You can encode units into types, but it gets ugly fast once you do anything more complex than addition and multiplication, so no one does it actually. You won't find any matrix library that uses types to encode the measurement units of every element of a matrix the way you would in a regular physics computation.

The way measurement units are normally used is essentially like special dimensionless constants that algebraic operations except +/- work on normally. So, you can multiply measurement units, you can divide them, a measurement unit divided by itself equals 1, you can raise a measurement unit to a power etc.

I agree that units aren't types. However, I think there's validity to thinking about concepts such as acceleration vs. speed vs. mass etc. as distinct types.

Each of those can be specified with different units from different systems of measurement. Some of those are compatible with one another, given some transformations. E.g. for speed, one can convert X m/s into MPH: different units, but same type.

However, mass is incompatible with acceleration: there's no possible valid transformation for Y grams into m/^2. If I was writing a program, I would like the language to prevent me from putting in a mass value into a place where I need a velocity. If I was writing a physics "proof," it would similarly be invalid to intermix values from these two distinct concepts.

I agree that types are a decent way of representing measurement units for many common use cases.

But I think the difference between the two is more fundamental. It's true of course that you can't transform a mass into a speed.

However, the interesting thing is that you can multiply 5kg by 10 meters/second and get 50m×kg/s, and this is a meaningful operation (in this case, you get a momentum). You can then divide this by 5s and get 10m×kg/s² which is still meaningful (a change in momentum). Even more, you can now divide this by 5kg/s (a change in mass), and get 2m/s (speed).

The way multiplication and division work with measurement units, you can't easily define them as functions that take the measurement units of their parameters as types, since you'd constantly get new types. E.g. the type of `x = foldl (×) listOfMeterQuantties` would be `meter^len(listOfMeterQuantties)`. You could do this in a dependently-typed language of course, but it would be quite unnatural I think.

Essentially, the way you'd probably represent all this is to have a single type family that has a numeric parameter for every measurement unit you want to be able to represent. It would be something like PhysicalQuantity<X, Y, Z, W> == 1 m^X s^Y kg^Z k^W. + and - would be defined on pairs of PhysicalQuantity<X, Y, Z, W> and PhysicalQuantity<X, Y, Z, W>. × and / would be defined on pairs of PhysicalQuantity<X1, Y1, Z1, W1> and PhysicalQuantity<X2, Y2, Z2, W2> and they would produce PhysicalQuantity<X1+X2, Y1+Y2, Z1+Z2, W1+W2> (or - for division). How usable this would then be (i.e. the type of "1m" would be PhysicalQuantity<1,0,0,0>) is debatable. But even if it would be good enough, I think it is quite apparent that the type representation is nowhere near intuitive or direct.

> More refined, my claim is that it is a super powerful tool that brings substantial benefits. And that it's a mistake to not use this tool.

I mostly agree with this. I wouldn't say it's super powerful, but it's a super convenient tool that quickly eliminates a broad class of errors without that much effort or contortions in our programs. I do think that the sweetspot for types is something like OCaml or Rust, and that going even into Haskell style (monads) starts to expend too much effort on the types compared to functionality.

I am hopeful that other techniques will come along and complement types to more easily statically check more complex properties of our code. I've been hearing great things about TLA+ style property-based specifications that I'd like to try at some point.

> For instance, there's the Rust crate dfdx, which uses dependent typing to encode the shapes of tensors. [1]

I don't think shapes of tensors is a particularly complex property. It's nice that this is enforced, but I still see it in the area of very simple properties. Rust's borrow checking is actually a better example of a more complex property of a program being statically verified.

> This isn't quite right. At least, I think what you're saying is that "physics proofs don't set up typing rules therefore they don't use types." But then again, proofs aren't necessarily programs. Is every physics proof computable? I'm not a physicist so I'll defer that to an expert.

Physics is basically all about computation, and very little about proof. The point of physics is usually to compute a property of a physical system based on some model, then perform an experiment and measure the same property. If the measurement agrees with the computation, that's a "proof" that the model is "correct" (in quotes because of course these are not what we normally mean by those words in formal contexts).

And in those computations, physicists don't use types in any way you might see in a computer science paper in their computations. Measurement units are somewhat similar at a very high level, but they are used very differently in practice.

I go into a little more detail on this in [0].

[0] https://news.ycombinator.com/item?id=38692762

Thanks for a very thoughtful reply! (Feels like real HN. I appreciate that.)

It seems like we're not in too much disagreement. I also see Rust's borrow checker as a real engineering achievement. They were able to take lessons learned discovering affine type systems and apply in in a way that gives Rust programs some tremendously wonderful properties. Whether it's making sure that the ML code doesn't do something invalid or whether all of the code doesn't make memory errors, I still see a never-ending march of progress on investing more into type systems and static analysis.

I appreciate your insights on Physics. I understand enough that Quantum Physics takes the view (more or less, I believe!) that the universe is akin to a computer, with particles (bits) that behave in specific ways and determine how everything works (computation, if I can continue the metaphor).

I replied to your linked comment. But I think there's perhaps a misunderstanding of what types are. I agree: units aren't types. However, a

> a property of a physical system based on some model

counts as a value that has a type. Perhaps the whole understanding is that Physics has a _very complex type system_. Perhaps one that no one has invested in trying to make computable?

Yes, I think we agree quite a bit, and for me as well this is exactly the type of conversation I come to HN for.

I replied more in depth on the measurement units post on the specifics about that, so I'll leave it aside here.

> I appreciate your insights on Physics.

About physics though, I would say that when I'm talking about computations I'm not describing some complex or deep idea about the universe acting as a computer. I just mean that most of what you do as a physicist is simply to do computations, much like we would in school. You don't write proofs the way most mathematicians do: you take some functions (say, Newton's laws of motion) and an initial state, and compute the state of the system after some time or at some event. Your result is not a proof that X = Y, it is simply the value Y, which you didn't know beforehand. Ideally, you might write a program that automates this work for you, so that instead of doing a computation by hand, you ask a computer to do it for you.

> But I think there's perhaps a misunderstanding of what types are. I agree: units aren't types. However, a

>> a property of a physical system based on some model

> counts as a value that has a type.

I don't think this is the right way to look at it. Types are a specific concept in computer science/math and they act in certain ways. They are for example isomorphic to propositions in first order logic (the Church-Howard correspondence if I remember correctly), but that doesn't mean they are the same thing.

Reply on news.ycombinator.com