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

81–88 of 88 posts

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

#81

Post by lmm »

Kutta wrote: post #67
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…

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

Both State- and ST-using code is harder to understand than code that doesn't use them. Immutable semantics are easier to reason about. Of course the implementation of those semantics may involve mutation at some lower level. But ideally we would have a runtime system that could implement immutable semantics with no loss of efficiency compared to implementing those lower-level mutations explicitly in our code.

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

#82

Post by anentropic »

nikivi wrote: post #2

What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?

https://dl.acm.org/doi/10.1145/3371071

Dependent Types via macros, in Racket

somewhere near the end of the paper is a table of the macro features used, which gives the impression it was only possible in Racket, but the lack of a common terminology for these things makes it hard to compare other languages' macro systems unless you are deeply familiar with them, so maybe it could be adapted

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

#83

Post by Shoue »

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."

When dealing with corecursion (infinite streams) you don't care about whether you terminate, but rather, whether the infinite stream is _productive_ meaning it doesn't stop producing values. The prime example of a function that's impossible(?) to prove productive (for all cases) is filter – since it takes a predicate function that decides whether values are returned or not. If you give filter a predicate that always returns false you will never produce any values, hence that wouldn't be productive.

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

#84

Post by uryga »

icen wrote: post #77
ImprobableTruth wrote: post #73

Earlier quoted context omitted.

It's just standard dependent types. Types don't (necessarily) get erased, but all the type checking itself is done at compile time. I don't think it makes sense to think of it as specifically "statically kinded", since kinds (which are just types higher on the universe hierarchy) can also be present at runtime.

Indeed - the Type/Kind hierarchy is unified when you write a dependently typed system. In simply typed lambda calculus, you have a system of values, types, and kinds, which are required to make sense of the structure. In dependent types, you have values, and types, which are also values.

> Type/Kind hierarchy is unified when you write a dependently typed system

i'm being pedantic, but i don't think that's always the case. afaik

  Type : Type
leads to "inconsistency" (sounds like Russell's paradox, but my knowledge of the theory gets flaky here). so e.g. in Coq there's actually a hierarchy of "universes":

> "[The type of Int is Set, ] the type of Set is Type(0), the type of Type(0) is Type(1), the type of Type(1) is Type(2), and so on."

http://adam.chlipala.net/cpdt/html/Universes.html

(though a dependently-typed system may hide universes from the user by default and offer "universe polymorphism" to allow them to gloss over it)

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

#85

Post by mx00s »

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.

You're right, there are several notable improvements in Idris2. I was mainly referring to the amount of code from the book that must be adapted. The QTT features, as you say, are opt-in; by default no new constraints are imposed.

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

#86

Post by dependenttypes »

dan-robertson wrote: post #12
nikivi wrote: post #2

What language features are needed in order to implement dependent types? Can you implement it on top of existing features of say Rust or Swift?

A first feature is the ability to define “interesting” types. By interesting I mean “generic” types which do things depending on the types of their arguments. In other words, a way to have functions at the type level. In Haskell you can do this with type families. I don’t know if you can do something similar in rust (have a type in a trait and then implement that trait in certain cases to get your function from input…

> A first feature is the ability to define “interesting” types. By interesting I mean “generic” types which do things depending on the types of their arguments

LF does not have higher kinded types but it does have dependent types.

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

#87

Post by tzjmetron »

Legogris wrote: post #71
nilkn wrote: post #57

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

My experience is from 2015 but from a language-perspective the only things I personally saw lacking for prime-time use would be performance and the compiler/type-checker not always giving accurate error messages - but overall, nothing considerable when comparing to Haskell. I don't know how much those areas have been improving since. Overall I was very excited about Idris and found the syntax a lot more approachable…

Precisely my experience as well! I also wish Edwin would get some sort of corporate backing so that Idris could be funded to get into production-ready mode. Idris2 is much faster (both compilation wise as well as execution wise) than Idris1, but the standard library is not done (as are parts of the language itself).

I would love to be able to write production code in Idris rather than patching together a million Haskell extensions.

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

#88

Post by tzjmetron »

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…

Just like the GC-vs-non-GC debate, emotions like yours are perfectly understandable, if not fully justifiable. We are humans, after all.
Post reply on HN