3 ms·

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?

fabianhjr 6y ago
Not really, Idris2 is very similar to Idris1 and the book is more on developing concepts/ideas rather than just being a cookbook of things to do in Idris1.
kccqzy 6y ago
That book pretty much teaches just the basics. The basics have not changed.
mx00s 6y ago
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 https://idris2.readthedocs.io/en/latest/typedd/typedd.html [2] https://github.com/idris-lang/Idris2/tree/master/tests/typedd-book https://github.com/idris-lang/Idris2/tree/master/tests/typed...
- schr0dinger 6y ago
  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.
  - zelphirkalt 6y ago
    The Idris 2 compiler is build with Chez Scheme? That's pretty cool in my opinion, didn't know that.
    - mjepronk 6y ago
      It compiles to Chez Scheme. It's written in Idris 2 (self-hosted).
    - rq1 6y ago
      It is written with Idris2 as the article mentions. It produces/translates to Chez Scheme code.
  - mx00s 6y ago
    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.

fabianhjr 6y ago

Not really, Idris2 is very similar to Idris1 and the book is more on developing concepts/ideas rather than just being a cookbook of things to do in Idris1.

kccqzy 6y ago

That book pretty much teaches just the basics. The basics have not changed.

mx00s 6y ago

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 https://idris2.readthedocs.io/en/latest/typedd/typedd.html [2] https://github.com/idris-lang/Idris2/tree/master/tests/typedd-book https://github.com/idris-lang/Idris2/tree/master/tests/typed...

schr0dinger 6y ago
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.
- zelphirkalt 6y ago
  The Idris 2 compiler is build with Chez Scheme? That's pretty cool in my opinion, didn't know that.
  - mjepronk 6y ago
    It compiles to Chez Scheme. It's written in Idris 2 (self-hosted).
  - rq1 6y ago
    It is written with Idris2 as the article mentions. It produces/translates to Chez Scheme code.
- mx00s 6y ago
  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.