6 ms·

New JavaScript code generator in Idris 2

164 points by ska80 6y ago

spinningslate 6y ago
Aside from being an interesting feature, the discussion is a great example of positively encouraging contributions. There's a lot to admire about Edwin Brady: smart, kind, polite, self-effacing, committed. Given the prevalence of acrimony in online discourse - both mainstream and social media - it's always good to be reminded that there are lots of really decent people out there. And anyone who names a language after a dragon in a children's animation[0] gets my vote! [0] https://en.wikipedia.org/wiki/Ivor_the_Engine https://en.wikipedia.org/wiki/Ivor_the_Engine
- kryptiskt 6y ago
  Well, a lot of the thread is just me fumbling around with Github features.
guerrilla 6y ago
If you also didn't know Idris 2 was out, check here [1] for what's new. [1]. https://idris2.readthedocs.io/en/latest/updates/updates.html#sect-new-features https://idris2.readthedocs.io/en/latest/updates/updates.html...
madushan1000 6y ago
I wonder how much effort would it take to add a rust code generator. I'm guessing we can't add a C code generator because idris seems to need a garbage collector.
- gnulinux 6y ago
  Haskell used to be compiled to C. (not sure if they still use this backend, I think main GHC backend compiles to LLVM). "Doesn't have garbage collector" is not a good reason not to be able to compile to C, surely garbage collection can be implemented in C.
  - iso8859-1 6y ago
    Just because it is possible doesn't mean it's easy. If you implement garbage collection in C, you are using your own garbage collector, the C ecosystem doesn't support you in any way. When people make the argument of preferring a compilation target because it has a specific feature, they are not saying "target is not Turing complete, you can't implement this feature". They say "not natively supported and I would rather not implement this myself". And no, -fllvm exists, but it is not the default: https://downloads.haskell.org/~ghc/8.8.3/docs/html/users_guide/codegens.html#llvm-code-generator-fllvm https://downloads.haskell.org/~ghc/8.8.3/docs/html/users_gui...
  - pjmlp 6y ago
    GHC uses its own backend with C-- as intermediate language. The LLVM is just yet another one.
- andrepd 6y ago
  ? Why shouldn't a garbage collector be able to be implemented in C?
  - madushan1000 6y ago
    someone definatly can, but better programmers than I, have worked for years to get jvm, v8 GCs to get where they are. So I don't even want to try.
- kryptiskt 6y ago
  Idris 1 compiles via C, it just has to implement a garbage collector in its runtime system. It should be noted that Idris 1 has much worse performance than Idris 2 compiled to Chez Scheme, it would take a serious effort to do better than the current Chez backend. The logical target for a high-performance backend would be LLVM instead of rust. After elaboration Idris 2 has a series of intermediate languages, from lambda calculus to a simple register machine. Creating LLVM code from the least abstract of them wouldn't be any harder than creating Rust code.
  - madushan1000 6y ago
    I was thinking of rust specifically because of GC, I don't know how to write a GC and I don't even want to try. But if I use rust, I won't have to because of rust's zero cost abstractions.
    - icen 6y ago
      There seems to be a bit of confusion here. Idris doesn't provide the same tools and guarantees as Rust does to manage memory, and instead requires that implementations provide a garbage collector. If you're producing code for a collected language, you can forward on all of the allocations to that language, and if not, you will need to implement one. Zero-cost abstractions or not, Idris needs a GC from somewhere.
      - kryptiskt 6y ago
        Reference counting would go a long way though as there is very little mutation in a typical Idris program, so you could probably sew something together in Rust with Rc cells and a simple cycle detector. But basically, having true closures requires some kind of GC. That was already recognized in Steele's Lambda papers in the 70s. Rust has to make compromises with its closures to avoid that.
      - madushan1000 6y ago
        I was hoping I could get by without resolving to to GC, utilizing the rust allocation model(RAII with syntactic sugar and compiler helping out basically). If I "have to" write a GC because idris programming model requires is, I don't think there is a lot of value in writing a rust code generator.
- saurik 6y ago
  I somehow (incorrectly I guess) thought Idris was strict (as opposed to Haskell) specifically to avoid a requirement on a garbage collector :(.
  - sfvisser 6y ago
    These things are unrelated. Idris is strict and performs heap allocations so does require a GC.
- senorsmile 6y ago
  Naive question: does the new linear type support in Idris 2 get it closer to possibly not needing garbage collection?
ch4s3 6y ago
I've been interested in Idris for quite awhile, but not sure how to go about learning it. Are there any particularly good resources? Am I expected to know Haskell or is it sufficient to have a few years of experience with FP in general?
- mixedCase 6y ago
  You should be good to go picking up "Type-driven development with Idris". It's a great book not just for learning Idris but also for hammering down the concept of using types and the compiler as a design pillar if you're not fully used to it.
  - ch4s3 6y ago
    I've written some Elm so I think I basically get the concept. I'll have to check out the book then.
  - mkw5053 6y ago
    +1 on "Type-driven development with Idris". A really fun and insightful book to work through!
  - saityi 6y ago
    There's even a page in the Idris 2 docs with updates to the book for Idris 2 -- https://idris2.readthedocs.io/en/latest/typedd/typedd.html https://idris2.readthedocs.io/en/latest/typedd/typedd.html The book is otherwise still totally relevant for Idris 2 and is a great read & introduction to dependent types.
- lightgreen 6y ago
  https://learn-idris.net/ https://learn-idris.net/ this is the website I made. Not sure it is very good though. The Edwin’s book about Idris is good, BTW.
swagonomixxx 6y ago
Are there any examples of projects in Idris that do something non-trivial and non-academic? E.g, websites, video games, etc.
- DonaldPShimoda 6y ago
  Idris is primarily an academic language, much like Haskell. While I don't doubt that people will come to implement such programs in it at some point, I haven't seen anything yet (though I admittedly don't stick close to Idris at the moment so I could've missed something).
- saityi 6y ago
  Jan Corazza has some really great write-ups about writing bindings to SDL and writing a video game in Idris using them. The source is available on Github https://flowing.systems/2020/01/13/a-game-in-a-pure-language-part-1-introduction-and-problems-with-idris.html https://flowing.systems/2020/01/13/a-game-in-a-pure-language... https://flowing.systems/2020/04/13/a-game-in-a-pure-language-part-2-state.html https://flowing.systems/2020/04/13/a-game-in-a-pure-language... https://github.com/corazza/game-idris https://github.com/corazza/game-idris
- deleted 6y ago
  [deleted]
- leonvv 6y ago
  I wrote a Todo application in Idris that compiles to Javascript (https://github.com/leon-vv/Todo https://github.com/leon-vv/Todo). I used the dependent type system of Idris to embed a small part of SQL in Idris, which means the type system can proof certain things about my queries (for example that fields accessed are actually part of the (joined) tables).

164 points by ska80 6y ago

Aside from being an interesting feature, the discussion is a great example of positively encouraging contributions. There's a lot to admire about Edwin Brady: smart, kind, polite, self-effacing, committed. Given the prevalence of acrimony in online discourse - both mainstream and social media - it's always good to be reminded that there are lots of really decent people out there. And anyone who names a language after a dragon in a children's animation[0] gets my vote! [0] https://en.wikipedia.org/wiki/Ivor_the_Engine https://en.wikipedia.org/wiki/Ivor_the_Engine

kryptiskt 6y ago
Well, a lot of the thread is just me fumbling around with Github features.

guerrilla 6y ago

If you also didn't know Idris 2 was out, check here [1] for what's new. [1]. https://idris2.readthedocs.io/en/latest/updates/updates.html#sect-new-features https://idris2.readthedocs.io/en/latest/updates/updates.html...

madushan1000 6y ago

I wonder how much effort would it take to add a rust code generator. I'm guessing we can't add a C code generator because idris seems to need a garbage collector.

gnulinux 6y ago
Haskell used to be compiled to C. (not sure if they still use this backend, I think main GHC backend compiles to LLVM). "Doesn't have garbage collector" is not a good reason not to be able to compile to C, surely garbage collection can be implemented in C.
- iso8859-1 6y ago
  Just because it is possible doesn't mean it's easy. If you implement garbage collection in C, you are using your own garbage collector, the C ecosystem doesn't support you in any way. When people make the argument of preferring a compilation target because it has a specific feature, they are not saying "target is not Turing complete, you can't implement this feature". They say "not natively supported and I would rather not implement this myself". And no, -fllvm exists, but it is not the default: https://downloads.haskell.org/~ghc/8.8.3/docs/html/users_guide/codegens.html#llvm-code-generator-fllvm https://downloads.haskell.org/~ghc/8.8.3/docs/html/users_gui...
- pjmlp 6y ago
  GHC uses its own backend with C-- as intermediate language. The LLVM is just yet another one.
andrepd 6y ago
? Why shouldn't a garbage collector be able to be implemented in C?
- madushan1000 6y ago
  someone definatly can, but better programmers than I, have worked for years to get jvm, v8 GCs to get where they are. So I don't even want to try.
kryptiskt 6y ago
Idris 1 compiles via C, it just has to implement a garbage collector in its runtime system. It should be noted that Idris 1 has much worse performance than Idris 2 compiled to Chez Scheme, it would take a serious effort to do better than the current Chez backend. The logical target for a high-performance backend would be LLVM instead of rust. After elaboration Idris 2 has a series of intermediate languages, from lambda calculus to a simple register machine. Creating LLVM code from the least abstract of them wouldn't be any harder than creating Rust code.
- madushan1000 6y ago
  I was thinking of rust specifically because of GC, I don't know how to write a GC and I don't even want to try. But if I use rust, I won't have to because of rust's zero cost abstractions.
  - icen 6y ago
    There seems to be a bit of confusion here. Idris doesn't provide the same tools and guarantees as Rust does to manage memory, and instead requires that implementations provide a garbage collector. If you're producing code for a collected language, you can forward on all of the allocations to that language, and if not, you will need to implement one. Zero-cost abstractions or not, Idris needs a GC from somewhere.
    - kryptiskt 6y ago
      Reference counting would go a long way though as there is very little mutation in a typical Idris program, so you could probably sew something together in Rust with Rc cells and a simple cycle detector. But basically, having true closures requires some kind of GC. That was already recognized in Steele's Lambda papers in the 70s. Rust has to make compromises with its closures to avoid that.
    - madushan1000 6y ago
      I was hoping I could get by without resolving to to GC, utilizing the rust allocation model(RAII with syntactic sugar and compiler helping out basically). If I "have to" write a GC because idris programming model requires is, I don't think there is a lot of value in writing a rust code generator.
saurik 6y ago
I somehow (incorrectly I guess) thought Idris was strict (as opposed to Haskell) specifically to avoid a requirement on a garbage collector :(.
- sfvisser 6y ago
  These things are unrelated. Idris is strict and performs heap allocations so does require a GC.
senorsmile 6y ago
Naive question: does the new linear type support in Idris 2 get it closer to possibly not needing garbage collection?

ch4s3 6y ago

I've been interested in Idris for quite awhile, but not sure how to go about learning it. Are there any particularly good resources? Am I expected to know Haskell or is it sufficient to have a few years of experience with FP in general?

mixedCase 6y ago
You should be good to go picking up "Type-driven development with Idris". It's a great book not just for learning Idris but also for hammering down the concept of using types and the compiler as a design pillar if you're not fully used to it.
- ch4s3 6y ago
  I've written some Elm so I think I basically get the concept. I'll have to check out the book then.
- mkw5053 6y ago
  +1 on "Type-driven development with Idris". A really fun and insightful book to work through!
- saityi 6y ago
  There's even a page in the Idris 2 docs with updates to the book for Idris 2 -- https://idris2.readthedocs.io/en/latest/typedd/typedd.html https://idris2.readthedocs.io/en/latest/typedd/typedd.html The book is otherwise still totally relevant for Idris 2 and is a great read & introduction to dependent types.
lightgreen 6y ago
https://learn-idris.net/ https://learn-idris.net/ this is the website I made. Not sure it is very good though. The Edwin’s book about Idris is good, BTW.

swagonomixxx 6y ago

Are there any examples of projects in Idris that do something non-trivial and non-academic? E.g, websites, video games, etc.

DonaldPShimoda 6y ago
Idris is primarily an academic language, much like Haskell. While I don't doubt that people will come to implement such programs in it at some point, I haven't seen anything yet (though I admittedly don't stick close to Idris at the moment so I could've missed something).
saityi 6y ago
Jan Corazza has some really great write-ups about writing bindings to SDL and writing a video game in Idris using them. The source is available on Github https://flowing.systems/2020/01/13/a-game-in-a-pure-language-part-1-introduction-and-problems-with-idris.html https://flowing.systems/2020/01/13/a-game-in-a-pure-language... https://flowing.systems/2020/04/13/a-game-in-a-pure-language-part-2-state.html https://flowing.systems/2020/04/13/a-game-in-a-pure-language... https://github.com/corazza/game-idris https://github.com/corazza/game-idris
deleted 6y ago
[deleted]
leonvv 6y ago
I wrote a Todo application in Idris that compiles to Javascript (https://github.com/leon-vv/Todo https://github.com/leon-vv/Todo). I used the dependent type system of Idris to embed a small part of SQL in Idris, which means the type system can proof certain things about my queries (for example that fields accessed are actually part of the (joined) tables).