7 ms·

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

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.

cflewis 6y ago
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.
Buttons840 6y ago
It's worth noting that the book is written by the creator of Idris.
dejj 6y ago
> pass types as parameters to be altered during execution Wouldn't that be at odds with static typing?
- icen 6y ago
  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.
  - dejj 6y ago
    > you don't know which type you will actually get ahead of time Sounds like it's statically kinded, and dynamically typed. Or is it a place between kinds and types at which Idris operates?
    - ImprobableTruth 6y ago
      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.
      - icen 6y ago
        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.
        uryga 6y ago
        > 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 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)

cflewis 6y ago

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.

Buttons840 6y ago

It's worth noting that the book is written by the creator of Idris.

dejj 6y ago

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

icen 6y ago
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.
- dejj 6y ago
  > you don't know which type you will actually get ahead of time Sounds like it's statically kinded, and dynamically typed. Or is it a place between kinds and types at which Idris operates?
  - ImprobableTruth 6y ago
    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.
    - icen 6y ago
      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.
      - uryga 6y ago
        > 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 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)