5 ms·

Thanks for the link. I've been wondering how to lift N-D operations into the type system. If I write with NumPy x = r_[:n].reshape((3, -1, n/15))[:, :2].sum(

Thanks for the link. I've been wondering how to lift N-D operations into the type system. If I write with NumPy x = r_[:n].reshape((3, -1, n/15))[:, :2].sum(axis=-1) a compiler could figure out that the shape of x is (3, 2) and allow y = x + randn(m, 1, 2) while forbidding z = y - r_[:7] With NumPy you have to wait for a runtime error, and only if the shapes can't be broadcast. We're not even talking correct use of dimensions, etc. I suppose this may have been tackled in Haskell in the Repa library, but I'd need to read papers like http://benl.ouroborus.net/papers/repa/repa-icfp2010.pdf http://benl.ouroborus.net/papers/repa/repa-icfp2010.pdf to know. Hence my question if we could lift this into the type system in a conventional language, but I don't think it's possible in a general way.

thinkpad20 12y ago
I'm not sure what the notation you're using represents, but it looks like you're talking about matrices of a known size. What that's an example of is dependent types, where types can be parameterized by values, and not just types. For example, a (2D) matrix is parameterized by what it contains, and its dimensions. The former is a type but the latter are values. Without dependent types (or some subset of their capability) you can't represent this matrix type; you'd just have to check at runtime that no out-of-bounds access was occurring, so no; I don't think you could put this in a conventional language (without some crazy gymnastics, perhaps involving macros or similar). However, with dependent types, this is absolutely possible to statically guarantee that no out-of-bounds access will occur at runtime.