3 ms·

Very nice, haven't heard of this before. I think an ideal target for a dependently typed language is scientific array programming, so that you can ensure the s

Very nice, haven't heard of this before. I think an ideal target for a dependently typed language is scientific array programming, so that you can ensure the sizes of your matrix and array operations check out before performing long-running tasks. If a good array library can be built (e.g. port Haskell's Repa) then it might provide a great foundation for this.

dons 15y ago
With type level naturals recently added to GHC, statically checked arrays are already implementable in Haskell. * http://hackage.haskell.org/package/vector-static http://hackage.haskell.org/package/vector-static * http://hackage.haskell.org/package/hmatrix-static http://hackage.haskell.org/package/hmatrix-static A nice next step would be to optimize out additional runtime bounds checks.
- radarsat1 15y ago
  Very nice! I really look forward to using something like that.