Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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

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.



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.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: