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

61–70 of 88 posts

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

#61

Post by Reelin »

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-…

Would it be correct to describe Rust's generics as parametrically polymorphic templates then? I'm still not seeing how C++ templates aren't proper generics though - parametric polymorphism isn't a requirement for that, is it?

I guess I had mistakenly thought that run time dispatch and a single binary implementation was somehow required for parametric polymorphism since it requires treating all types identically. Upon reflection I can see that it's not actually exclusive of compile time dispatch though.

From a pragmatic perspective it seems unfortunate that such generics can't be used in an API without corresponding access to the source code. I saw the ability to work with arbitrary future types at runtime as largely being the point of type erasure.

From a theoretical perspective I'm having some trouble accepting the idea that Rust generics are an example of true parametric polymorphism. In the earlier example a function could behave differently based on the size of the type. That's not uniformly dispatching to a behavior implemented by the type though, which seems like the core idea behind parametric polymorphism to me. (I suppose my concerns are purely academic though. AFAIK runtime reflection in Java allows utterly breaking type erasure but in practice Java generics still seem to be referred to as an example of parametric polymorphism.)

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

#62

Post by schr0dinger »

mx00s wrote: post #58
cflewis wrote: post #33

Earlier quoted context omitted.

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…

Well minor including the switch to use of so called “quantitative type theory” where you can include use counts for variables that inform the compiler how long variables will stick around. Also the compiler switch to Chez Scheme yields a pretty big performance boost.

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

#63

Post by vaylian »

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…

Computer hardware has no concept of immutability or local state on the hardware level. You only have memory regions. If you want to get a feeling for this, I suggest to start learning assembly language.

Even if computers had immutable memory, then you still need to initialize memory regions with constant values and that would be a mutation.

It is possible to protect memory regions from writing, but these regions are still writable by the operating system kernel. And this is purely for safety and not for performance.

(And don't get me started on CPU caches and registers)

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

#64

Post by zelphirkalt »

schr0dinger wrote: post #62
mx00s wrote: post #58

Earlier quoted context omitted.

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…

Well minor including the switch to use of so called “quantitative type theory” where you can include use counts for variables that inform the compiler how long variables will stick around. Also the compiler switch to Chez Scheme yields a pretty big performance boost.

The Idris 2 compiler is build with Chez Scheme? That's pretty cool in my opinion, didn't know that.

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

#65

Post by mjepronk »

zelphirkalt wrote: post #64
schr0dinger wrote: post #62

Earlier quoted context omitted.

Well minor including the switch to use of so called “quantitative type theory” where you can include use counts for variables that inform the compiler how long variables will stick around. Also the compiler switch to Chez Scheme yields a pretty big performance boost.

The Idris 2 compiler is build with Chez Scheme? That's pretty cool in my opinion, didn't know that.

It compiles to Chez Scheme. It's written in Idris 2 (self-hosted).

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

#66

Post by zelphirkalt »

drcode wrote: post #10
krapht wrote: post #3

Earlier quoted context omitted.

I'm not sure that this question even makes sense. It's like asking: "What language features are needed in order to implement a borrow checker?" You don't bolt this functionality on to an existing language; it requires changes to your whole compiler pipeline to be useful.

Don't be so certain, some languages allow a lot of flexibility within libraries. For instance, Clojure has an excellent library implementing Go-style channels with green threads (core.async) all built without any modifications to the core system.

Good point, Lispy languages with sufficiently powerful macro systems can do this. This is part of the reason, why no language committee deciding on backwards compatible changes to the language is needed to develop such a library.

I don't know enough to say whether this would be possible in Rust.

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

#67

Post by Kutta »

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…

Immutability is an implementation detail with no inherent value. What we actually care about is referential transparency, encapsulation & tracking of effects, performance, abstraction, thread/type/memory safety, etc. The State monad in Haskell is implemented without mutation, but presents an API with mutation. The ST monad is implemented with mutation but presents a pure and referentially transparent external API.

It is fair to say that functional programming is primrarily in favor of immutable data structures because it is simpler to implement them efficiently in a setting where referential transparency is the default. Mutation (meaning referential intrasparency) is just more complicated, and we need heavier machinery to structure it nicely. We may use linear/substructural types, uniqueness types, regions, etc for this purpose, but here are a number of choices, and the picture is not as clear-cut as with plain pure lambda calculi. Just remember that mutation is not bad by itself, many functional programmers are often happy to speed up production code with mutation, it's just that it is usually more complicated to structure nicely.

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

#68

Post by rq1 »

zelphirkalt wrote: post #64
schr0dinger wrote: post #62

Earlier quoted context omitted.

Well minor including the switch to use of so called “quantitative type theory” where you can include use counts for variables that inform the compiler how long variables will stick around. Also the compiler switch to Chez Scheme yields a pretty big performance boost.

The Idris 2 compiler is build with Chez Scheme? That's pretty cool in my opinion, didn't know that.

It is written with Idris2 as the article mentions.

It produces/translates to Chez Scheme code.

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

#69

Post by dejj »

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.

> pass types as parameters to be altered during execution

Wouldn't that be at odds with static typing?

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

#70

Post by icen »

dejj wrote: post #69
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.

> pass types as parameters to be altered during execution Wouldn't that be at odds with static typing?

Dependent types let you do this. The type system ensures that you have all the types known at every point, and everything is sewn up before runtime - even though you don't know which type you will actually get ahead of time.

Types are values, and types can depend on values - so if your protocol tells you you should be getting a string, a string shows up in the type signature.

Post reply on HN