Comment on Idris - pure functional programming language with dependent typesparentComments−dons14yWith 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/hmatrix-staticA nice next step would be to optimize out additional runtime bounds checks.−radarsat114yVery nice! I really look forward to using something like that.
Comments
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/hmatrix-static
A nice next step would be to optimize out additional runtime bounds checks.
Very nice! I really look forward to using something like that.