News for hackers. Stuff that matters.
Re:Idris - pure functional programming language with depende... by dons on Thursday January 19, 2012 @09:58AM (#3484699)
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.

Re:Idris - pure functional programming language with depende... by radarsat1 on Friday January 20, 2012 @03:55PM (#3491180)
Very nice! I really look forward to using something like that.