Very nice, haven't heard of this before. I think an ideal target for a dependent... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		radarsat1 on Jan 19, 2012 \| parent \| context \| favorite \| on: Idris - pure functional programming language with ... 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 on Jan 19, 2012 [–]

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.

radarsat1 on Jan 20, 2012 | [–]

Very nice! I really look forward to using something like that.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact