Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why is Idris 2 so much faster than Idris 1?

type-driven.org.uk

Post reply on HN
Print view View original

51–60 of 88 posts

Re: Why is Idris 2 so much faster than Idris 1?

#51

Post by jinwoo68 »

pittma wrote: post #45
jinwoo68 wrote: post #37

Earlier quoted context omitted.

Idris does support forever loops or servers without losing totality. See https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.h...

Hm, that's not how I'm reading this. An infinite loop is, by definition, partial. What I'm gathering from this is that that stuckness that the typechecker can encounter in the face of partiality is okay in Idris, that its typechecker just says, "welp, this is as far as I go."

I’m specifically talking about the “Produces a non-empty, finite, prefix of a possibly infinite result” part on that page. As long as your server generates finite responses in finite times, Idris recognizes your code as total.

Re: Why is Idris 2 so much faster than Idris 1?

#52

Post by ncmncm »

neutronicus wrote: post #48
Reelin wrote: post #30

Earlier quoted context omitted.

What do you mean by C++ templates not really being generics? Aren't Rust's generics also implemented as templates (as opposed to parametric polymorphism)?

Rust Generics are Parametric Polymorphism - you must pre-declare the allowed operations on the Type Parameters via Trait Bounds (essentially Haskell Typeclass constraints), and the Generic will fail to compile if you try to perform any other operations in the body (even if the Generic is never instantiated). In C++ you can do any syntactically valid thing with the Type Parameter in a Template body, and it isn't type-…

... which does also happen at compile time. Or before you instantiate it, if the template is declared using concepts, in C++20.

The effect without concepts is that you can (in principle) get things that "accidentally" match, like applying "+" to strings; and that the error messages when they don't match are unpleasant. Concepts resolve both.

Re: Why is Idris 2 so much faster than Idris 1?

#53

Post by toastal »

I find this slightly depressing that using global mutable state had such a significant performance given the functional programming (encompassing Idris) is very much in favor of immutable data structures and purity. I know it's best to explicitly switch to mutability iff a bottleneck is found (like how `mut` is explicit and not default in Rust), but I want to believe that Idris can live in a purity. This makes me think my opinions are not far off from religion.

Re: Why is Idris 2 so much faster than Idris 1?

#54

Post by [deleted] »

xuejie wrote: post #38

The author first goes with: > Idris 1 is implemented in Haskell, but that has little (if anything) to do with the difference. But latter they also go on to say: > Idris 2 benefits from a robust, well-engineered and optimised run time system, by compiling to Chez Scheme. I must say I'm slightly confused here. Yes a rewrite might also enable to avoid all the legacy part that might slow down the code, but what is also p…

[deleted]

Re: Why is Idris 2 so much faster than Idris 1?

#55

Post by xuejie »

xuejie wrote: post #38

The author first goes with: > Idris 1 is implemented in Haskell, but that has little (if anything) to do with the difference. But latter they also go on to say: > Idris 2 benefits from a robust, well-engineered and optimised run time system, by compiling to Chez Scheme. I must say I'm slightly confused here. Yes a rewrite might also enable to avoid all the legacy part that might slow down the code, but what is also p…

Thanks guys for the explanation! I truly have misunderstood this post.

Re: Why is Idris 2 so much faster than Idris 1?

#57

Post by nilkn »

How practical is Idris (or Idris 2) for real-world production programming right now? It seems to be a pretty natural evolution of Haskell with dependent types built in from the ground up instead of being sort of achievable with a patchwork of language extensions. Moreover, making laziness optional is a big deal for real-world industrial applications. (Note that even the author of this post indicates at the end significant difficulty with space leaks in the original Haskell compiler for Idris.)

Or, said differently, what's missing in the language or ecosystem to make it more immediately practical? Could Idris be the successor to Haskell with appropriate support?

Re: Why is Idris 2 so much faster than Idris 1?

#58

Post by mx00s »

cflewis wrote: post #33
ngngngng wrote: post #5

I bought the book "Type Driven Development in Idris" and got several chapters in before getting distracted by whatever else. It was enough that I'm now annoyed relatively often that I can't pass types as parameters to be altered during execution. I really think they're onto something brilliant. I need to pick it back up and finish the book.

Hmm. My interest is piqued but this book is from 2017 and I am wondering if it is not horribly out of date at this point. WDYT?

There are some minor changes, but they are documented in detail [1]. The Idris2 repository maintains tests to detect any further divergence from the book [2].

I highly recommend the book. Typing in examples and getting experience collaborating with the compiler on edits is worthwhile. Even if you never use Idris(2) again after reading it, the demos on creating state machine DSLs with contextual invariants will leave a lasting impression.

[1] https://idris2.readthedocs.io/en/latest/typedd/typedd.html

[2] https://github.com/idris-lang/Idris2/tree/master/tests/typed...

Re: Why is Idris 2 so much faster than Idris 1?

#59

Post by sfj »

ncmncm wrote: post #50

The usual answer for such a question about X2 and X1 is that X1 was really slow. It is usually correct, with the proviso that X2 might still be really slow, only less so. With most computer artifacts, it is hard to tell, prima facie , that they are slow, until somebody makes a faster one. Then the original comes to be recognized as slow (although somebody will still insist it's not that slow). The faster one might st…

Compared to Haskell, it was slow indeed.

Re: Why is Idris 2 so much faster than Idris 1?

#60

Post by mbrock »

toastal wrote: post #53

I find this slightly depressing that using global mutable state had such a significant performance given the functional programming (encompassing Idris) is very much in favor of immutable data structures and purity. I know it's best to explicitly switch to mutability iff a bottleneck is found (like how `mut` is explicit and not default in Rust), but I want to believe that Idris can live in a purity. This makes me thi…

I think you need to see it as something like, the idea is that immutable data structures and purity are considered an excellent base layer for defining code, like also in math where integrals and differential equations are "purely functional" even though they implement or describe "phenomena of mutation." Mutable arrays are present in Haskell, they are just described on the linguistic level with immutable purity.
Post reply on HN