5 ms·

> Can the typechecker ensure that your matrices have compatible dimensions to be multiplied together? In any dependently typed language, absolutely yes.

tormeh 12y ago
Sorry, I forgot to specify that I meant matrices you read at runtime, for example from a csv.
- DerpDerpDerp 12y ago
  Haskell has a very neat interface for this, in that you build a special type which remembers the dimensions of a matrix as you build them, and then return either the result or a failure. 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.
- Dewie 12y ago
  What does it matter? No type-system will magically know ahead of time what the contents of the file will be before you run the program, but it can force you to do the appropriate checks when you do read it from the file.
  - chriswarbo 12y ago
    > No type-system will magically know ahead of time what the contents of the file will be before you run the program. Yes they can, it's known as 'type providers'. http://blogs.msdn.com/b/dsyme/archive/2013/01/30/twelve-type-providers-in-pictures.aspx http://blogs.msdn.com/b/dsyme/archive/2013/01/30/twelve-type...
deleted 12y ago
[deleted]
seanmcdirmid 12y ago
Except Haskell isn't dependently typed, right? I can do it in C# for small matrices, by including the dimensions as type bindings (http://bling.codeplex.com 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-Matrix.html 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?
- nightski 12y ago
  Actually Haskell does have some dependently typed features (and is being extended constantly). The reason it isn't used in that particular package is a mystery, except that a lot of these things are very new and Haskell is an evoloving ecosystem. That particular package simply may not have a release that uses all the latest GHC features. 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_Tutorial http://www.haskell.org/haskellwiki/Numeric_Haskell:_A_Repa_T...
  - seanmcdirmid 12y ago
    Dimensionality is easy, its the lengths of these dimensions that are hard. E.g. you can multiply n by k, k by m matrices to get an n by m matrix, but anything else is a type error. In Bling, I had Matrix<LN,LK> * Matrix<LK,LM> => Matrix<LN,LM>, where LN,LK,LM are type parameters up to around 10 (L0, L1, ..., L10, enough to do 3D graphics, mostly, but wouldn't work for HPC where lengths are much longer and diverse). Looking at the linked page, extent isn't a part of a matrix's type signature, so it would be checked dynamically, correct?
    - freyrs3 12y ago
      > you can multiply n by k, k by m matrices to get an n by m matrix, but anything else is a type error. This is exactly how Repa works, it uses a Peano encoding of the extent of dimensions to make invalid array operations inexpressible.

tormeh 12y ago

Sorry, I forgot to specify that I meant matrices you read at runtime, for example from a csv.

DerpDerpDerp 12y ago
Haskell has a very neat interface for this, in that you build a special type which remembers the dimensions of a matrix as you build them, and then return either the result or a failure. 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.
Dewie 12y ago
What does it matter? No type-system will magically know ahead of time what the contents of the file will be before you run the program, but it can force you to do the appropriate checks when you do read it from the file.
- chriswarbo 12y ago
  > No type-system will magically know ahead of time what the contents of the file will be before you run the program. Yes they can, it's known as 'type providers'. http://blogs.msdn.com/b/dsyme/archive/2013/01/30/twelve-type-providers-in-pictures.aspx http://blogs.msdn.com/b/dsyme/archive/2013/01/30/twelve-type...

deleted 12y ago

[deleted]

seanmcdirmid 12y ago

Except Haskell isn't dependently typed, right? I can do it in C# for small matrices, by including the dimensions as type bindings (http://bling.codeplex.com 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-Matrix.html 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?

nightski 12y ago
Actually Haskell does have some dependently typed features (and is being extended constantly). The reason it isn't used in that particular package is a mystery, except that a lot of these things are very new and Haskell is an evoloving ecosystem. That particular package simply may not have a release that uses all the latest GHC features. 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_Tutorial http://www.haskell.org/haskellwiki/Numeric_Haskell:_A_Repa_T...
- seanmcdirmid 12y ago
  Dimensionality is easy, its the lengths of these dimensions that are hard. E.g. you can multiply n by k, k by m matrices to get an n by m matrix, but anything else is a type error. In Bling, I had Matrix<LN,LK> * Matrix<LK,LM> => Matrix<LN,LM>, where LN,LK,LM are type parameters up to around 10 (L0, L1, ..., L10, enough to do 3D graphics, mostly, but wouldn't work for HPC where lengths are much longer and diverse). Looking at the linked page, extent isn't a part of a matrix's type signature, so it would be checked dynamically, correct?
  - freyrs3 12y ago
    > you can multiply n by k, k by m matrices to get an n by m matrix, but anything else is a type error. This is exactly how Repa works, it uses a Peano encoding of the extent of dimensions to make invalid array operations inexpressible.