In any dependently typed language, absolutely yes.
In any dependently typed language, absolutely yes.
I can do it in C# for small matrices, by including the dimensions as type bindings (http://bling.codeplex.com), but that is not practical for larger matrices, nor would it work for matrices loaded from IO.
To the downvoters: are you claiming Haskell is dependently typed? If so, why isn't it used in http://hackage.haskell.org/package/matrix-0.2.1/docs/Data-Ma...? Or just one matrix data type that checks dimension lengths via the type system?
Repa for instance does provide type errors based on dimensionality of matrices. This is a package on Hackage.
See http://www.haskell.org/haskellwiki/Numeric_Haskell:_A_Repa_T...
Looking at the linked page, extent isn't a part of a matrix's type signature, so it would be checked dynamically, correct?
This is exactly how Repa works, it uses a Peano encoding of the extent of dimensions to make invalid array operations inexpressible.
It's very simple to build a function which doesn't have to understand the possible dimension conflicts and lift it to work on this new type, returning an either (or a maybe, if there's only one failure mode) in place of a definite value.
It's also very simple to propagate such errors forward, so they'll short circuit a computation when you have non-matching matrices used in a calculation that's multiple steps.
In Haskell, I don't have to remember to write special functions which guard against this: I write functions that operate on the matrices and add the guarding at the very end. I can ensure that all my calls use the guarding functions, because they have a different type signature.
Trying to do this same thing in Python require that I remember to always use the guarded calls, and doesn't have as clean of an interface to create the guarded functions from standard functions.
Yes they can, it's known as 'type providers'. http://blogs.msdn.com/b/dsyme/archive/2013/01/30/twelve-type...