5 ms·

The problem is that linear algebra is probably one of the most basic things you can do with a computer. If static typing isn't capable of offering useful help o

The problem is that linear algebra is probably one of the most basic things you can do with a computer. If static typing isn't capable of offering useful help or even just has a few weird wrinkles, then something is very odd. For what it's worth, I've seen LA done in C++ with various templates and libraries, and so it's certainly possible in various ways.

nbouscal 12y ago
It wouldn't surprise me at all if static typing was capable of offering useful help. If it can't today, I wouldn't be surprised to see us make progress over the next few years. I think interesting conversations could be had about why this problem is harder to model using type systems than other problems are. Where I get confused is when this is used as an argument against using static typing in general. By analogy: “Hammering nails is probably one of the most basic things you can do as a carpenter. If lathes aren't capable of offering useful help, then something is very odd.” I don't mean to mock, but it doesn't seem odd to me at all that not all tools are good for all purposes. What seems odd to me is trying to argue against the use of a tool that has proven itself in many different situations by pointing out that there exist situations it isn't useful in. Sure, that's true, but so what?
- metaphorm 12y ago
  but a programming language isn't a hammer or a lathe. its a workshop that is used to produce hammers and lathes and every other tool you will need. the criteria for judging the workshop is rather different than the criteria for judging the lathe.
  - Solarsail 12y ago
    PL's as tools is a half-accurate analogy. If you're going to stretch it that far, shouldn't you use something more accurate? Or better, not use an analogy for something that detailed? Say, PL's are materials. They are something that useful things "tools" are fashioned out of. The properties of a material affect the entire thing built out of it, in modest but pervasive ways. Some programs are built in more than one language, this could be seen as an object built with different materials for different parts. Now, whether mainstream languages are analogous to different iron alloys, wood, concrete or plastic is a different discussion. (And maybe another exercise in taking an analogy too far...) Not sure where I saw this analogy first, since I can't find it on LtU...
  - deleted 12y ago
    [deleted]
- tome 12y ago
  > I think interesting conversations could be had about why this problem is harder to model using type systems than other problems are. We can summarize this in ten seconds: More equations hold between combinations of units than combinations of types constructed using type constructors. For example, m kg m^-1 = kg, but no such relationship exists between (A, (B, A -> R)) and B. Proving these sorts of equivalences adds complexity to type systems.
ThatGeoGuy 12y ago
I think you glossed over the point of the article in general. The author isn't asking whether Linear Algebra can be encoded into a static type system, hell, we had Fortran over 50 years ago! What the author is asking is whether the static type system can reasonably check the units of each member within a matrix or vector. Let's go over a short example: Assume that you have a matrix A, which contains several rows corresponding to measurements, and several columns corresponding to the partials in x (such as in the generic parametric least-squares problem => A * x - b = r, where we want to minimize r^2). What the author is asking is whether or not the static type-checker can manage units and conversions within each element of the matrix. Let's say the first 10 rows of A correspond to units of metres, while the next 10 correspond to angular units (i.e. radians or degrees). The solution of such a system is: x = -(A' * A)^-1 * A' * b What the author desires is a way to enforce that the units of the elements of A are maintained, similar to if you had: LengthInMetres a = LengthInMetres 1 + LengthInInches2; Where addition between LengthInMetres and LengthInInches would perform the appropriate conversion if need be, or else you would raise an error for a type contract violation. Currently, there isn't any system that encodes the types of each row, column, or even the individual elements within a matrix, which is why the author is raising the question whether or not it's possible for a type system such as Haskell's to do so. Right now, the best I've seen is linear algebra packages that can template over the internal type, but represents everything as doubles, or a number type of some kind. Numpy has some ability to modify internal data types (such as representing a matrix where each row is a tuple type or some other), but there is: 1. No static enforcement of type contracts in Numpy (more specifically Python) 2. Numpy does not provide the full set of matrix functionality if types are not the standard numeric types (obviously, you can't take the determinant of some arbitrary `object`, even if internally it represents an integer in metres). Overall, what the author raised is an interesting question, and makes me wonder if we'll ever get to such a point in the future. Of course, seeing as most matrix libraries are built on top of BLAS / ATLAS / LAPACK / MKL, it's doubtful that we'll see any high-performance linear algebra with smart type systems. EDIT: Formatting
GFK_of_xmaspast 12y ago
The type in actual numerical implementations tends to be 'double' or 'real'.

nbouscal 12y ago

It wouldn't surprise me at all if static typing was capable of offering useful help. If it can't today, I wouldn't be surprised to see us make progress over the next few years. I think interesting conversations could be had about why this problem is harder to model using type systems than other problems are. Where I get confused is when this is used as an argument against using static typing in general. By analogy: “Hammering nails is probably one of the most basic things you can do as a carpenter. If lathes aren't capable of offering useful help, then something is very odd.” I don't mean to mock, but it doesn't seem odd to me at all that not all tools are good for all purposes. What seems odd to me is trying to argue against the use of a tool that has proven itself in many different situations by pointing out that there exist situations it isn't useful in. Sure, that's true, but so what?

metaphorm 12y ago
but a programming language isn't a hammer or a lathe. its a workshop that is used to produce hammers and lathes and every other tool you will need. the criteria for judging the workshop is rather different than the criteria for judging the lathe.
- Solarsail 12y ago
  PL's as tools is a half-accurate analogy. If you're going to stretch it that far, shouldn't you use something more accurate? Or better, not use an analogy for something that detailed? Say, PL's are materials. They are something that useful things "tools" are fashioned out of. The properties of a material affect the entire thing built out of it, in modest but pervasive ways. Some programs are built in more than one language, this could be seen as an object built with different materials for different parts. Now, whether mainstream languages are analogous to different iron alloys, wood, concrete or plastic is a different discussion. (And maybe another exercise in taking an analogy too far...) Not sure where I saw this analogy first, since I can't find it on LtU...
- deleted 12y ago
  [deleted]
tome 12y ago
> I think interesting conversations could be had about why this problem is harder to model using type systems than other problems are. We can summarize this in ten seconds: More equations hold between combinations of units than combinations of types constructed using type constructors. For example, m kg m^-1 = kg, but no such relationship exists between (A, (B, A -> R)) and B. Proving these sorts of equivalences adds complexity to type systems.

ThatGeoGuy 12y ago

I think you glossed over the point of the article in general. The author isn't asking whether Linear Algebra can be encoded into a static type system, hell, we had Fortran over 50 years ago! What the author is asking is whether the static type system can reasonably check the units of each member within a matrix or vector. Let's go over a short example: Assume that you have a matrix A, which contains several rows corresponding to measurements, and several columns corresponding to the partials in x (such as in the generic parametric least-squares problem => A * x - b = r, where we want to minimize r^2). What the author is asking is whether or not the static type-checker can manage units and conversions within each element of the matrix. Let's say the first 10 rows of A correspond to units of metres, while the next 10 correspond to angular units (i.e. radians or degrees). The solution of such a system is: x = -(A' * A)^-1 * A' * b What the author desires is a way to enforce that the units of the elements of A are maintained, similar to if you had: LengthInMetres a = LengthInMetres 1 + LengthInInches2; Where addition between LengthInMetres and LengthInInches would perform the appropriate conversion if need be, or else you would raise an error for a type contract violation. Currently, there isn't any system that encodes the types of each row, column, or even the individual elements within a matrix, which is why the author is raising the question whether or not it's possible for a type system such as Haskell's to do so. Right now, the best I've seen is linear algebra packages that can template over the internal type, but represents everything as doubles, or a number type of some kind. Numpy has some ability to modify internal data types (such as representing a matrix where each row is a tuple type or some other), but there is: 1. No static enforcement of type contracts in Numpy (more specifically Python) 2. Numpy does not provide the full set of matrix functionality if types are not the standard numeric types (obviously, you can't take the determinant of some arbitrary `object`, even if internally it represents an integer in metres). Overall, what the author raised is an interesting question, and makes me wonder if we'll ever get to such a point in the future. Of course, seeing as most matrix libraries are built on top of BLAS / ATLAS / LAPACK / MKL, it's doubtful that we'll see any high-performance linear algebra with smart type systems. EDIT: Formatting

GFK_of_xmaspast 12y ago

The type in actual numerical implementations tends to be 'double' or 'real'.