3 ms·

I've been learning Haskell and Idris off and on now for a few years. I have a few friends who happen to be computer science majors and they tend to be very dis

I've been learning Haskell and Idris off and on now for a few years. I have a few friends who happen to be computer science majors and they tend to be very dismissive of Haskell, they mostly focus on the performance tweaking of a Haskell program, which seems to be a 'black art'. Does anyone know if Idris improves on this aspect of Haskell?

hood_syntax 10y ago
Idris follows the eager evaluation model, so I would assume it's easier to reason about. I wouldn't take my word for it however
deleted 10y ago
[deleted]
thinkpad20 10y ago
I don't think Idris is nearly as performant as Haskell. Haskell has been around for way longer and has had piles of work done on optimizing the performance of the generated code, garbage collection, etc. Haskell can be written to be very fast, although its high-level nature and laziness can make it harder to optimize than a strict/imperative language. Idris on the other hand is still very much an experimental project more focused on practical applications of dependent type theory than things like performance. However, with enough work done on its compiler, its strictness and the abundance of type information might allow it to be eventually more performant. Though, the lack of type erasure might negatively impact performance as well depending on how types work at runtime...
icen 10y ago
Idris, unlike Haskell, is strict, which has the general effect of making Idris' performance a bit more predictable, and a bit more like programming in other languages. However, GHC is a phenomenal compiler, and can outperform Idris for many things; this is natural, as it's seen a lot of interest in terms of producing performant code. There are still some gotchas in Idris code. The biggest one that I can think of is indexing some type with data that doesn't manage to get erased (the usual type erasure algorithm is pretty aggressive, but it can't remove everything). Some of the most useful types for programming (as in, proving theorems about the code) are wonderfully inefficient (as an example, the inductive definition of natural number is an empty linked list - taking up plenty of space in pointers, and killing your cache whenever it's accessed - Idris knows about Nat, but not about other types). Operations on the data, which might look very efficient, can also end up operating on the indices, which might not be. Here's the docs explaining the possible hiccup with erasure: http://docs.idris-lang.org/en/latest/reference/erasure.html http://docs.idris-lang.org/en/latest/reference/erasure.html
- posterboy 10y ago
  >strict I am eager to point out, how lazy is to call lazy strict.

hood_syntax 10y ago

Idris follows the eager evaluation model, so I would assume it's easier to reason about. I wouldn't take my word for it however

deleted 10y ago

[deleted]

thinkpad20 10y ago

I don't think Idris is nearly as performant as Haskell. Haskell has been around for way longer and has had piles of work done on optimizing the performance of the generated code, garbage collection, etc. Haskell can be written to be very fast, although its high-level nature and laziness can make it harder to optimize than a strict/imperative language. Idris on the other hand is still very much an experimental project more focused on practical applications of dependent type theory than things like performance. However, with enough work done on its compiler, its strictness and the abundance of type information might allow it to be eventually more performant. Though, the lack of type erasure might negatively impact performance as well depending on how types work at runtime...

icen 10y ago

Idris, unlike Haskell, is strict, which has the general effect of making Idris' performance a bit more predictable, and a bit more like programming in other languages. However, GHC is a phenomenal compiler, and can outperform Idris for many things; this is natural, as it's seen a lot of interest in terms of producing performant code. There are still some gotchas in Idris code. The biggest one that I can think of is indexing some type with data that doesn't manage to get erased (the usual type erasure algorithm is pretty aggressive, but it can't remove everything). Some of the most useful types for programming (as in, proving theorems about the code) are wonderfully inefficient (as an example, the inductive definition of natural number is an empty linked list - taking up plenty of space in pointers, and killing your cache whenever it's accessed - Idris knows about Nat, but not about other types). Operations on the data, which might look very efficient, can also end up operating on the indices, which might not be. Here's the docs explaining the possible hiccup with erasure: http://docs.idris-lang.org/en/latest/reference/erasure.html http://docs.idris-lang.org/en/latest/reference/erasure.html

posterboy 10y ago
>strict I am eager to point out, how lazy is to call lazy strict.