Hacker News Reader

Comment by BucketSort | Hacker News Reader

I come from a statically typed background (C++), but have been doing a lot of analytics in python in the past two years. It is frustrating not to have compile time guarantees when dealing with mathematical programs, because some things have to be a particular type (i.e. matrices of compatible dimensions). The result is a copious use of asserts, but it feels bad when you know that if you did this in a functional language,let's say, you could prove implementations are correct by the nature of the type system. In short, I'd love to see more strong type support in python.

View on HN

>(i.e. matrices of compatible dimensions)

What language do you use where you can get these kinds of guarantees? As far as I know very few languages provide those kinds of dependent types statically.

C++ makes this possible via templates. Generally the size is moved to a template argument, which allows the compiler to check this at compile time (of course, this restricts you to statically sized matrices).

Good to know. I was apparently unaware how powerful templates were.

Don't feel too bad, almost everyone is. And almost all of the people who are aware of how "powerful" they are tend to equate "hellish complexity" with "expressive power" and are not people you want to work with.

There are a few shining exceptions, but not many.

https://stackoverflow.com/a/22645853

I think I knew that templates were Turing complete, but so are java generics, it's just that to get dependent types in generics you have to reinvent the integers within the generic system. Not so for templates, which I didn't realize. That's pretty nifty!

In graphics programming, you have specific types for lots of small vectors and matrices (for vectors, there are separate types for every sizes 4 and below, and matrices usually comes in a variety of sizes as well, at the very least 3x3, 3x4 and 4x4).

Typechecking is very useful here: if you try to transform a point in space represented by a Vector3 by a general 4x4 matrix, it fails compilation because you have to convert the point to homogeneous coordinates first. Very useful information from the type system.

I'm aware of that, I was more thinking in the general case, as comes up in machine learning for example, where you have sizes like 128, 192, and odd shapes like 12x3x100x100 4-tensors, etc.

That is, generalized matrix types, not simply rotation matrix types or whatnot for special cases.

Eigen (a popular matrix library) does it in c++.

I believe in the functional world, that sort of thing is implemented suing a feature called dependent types. It's not a very common feature, but Liquid Haskell implements it.

Reply on news.ycombinator.com