Hacker News new | ask | show | jobs
by seanmcdirmid 4390 days 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), 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?

1 comments

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_T...

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?

> 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.

Ok. This isn't obvious at all by looking at the documentation, also since extent doesn't seem to appear in the type signature of a matrix instance.