5 ms·

I discovered Idris when I was playing around with Agda last summer. It's cool to see a systems programming language with dependent types.

Dewie 13y ago
> It's cool to see a systems programming language with dependent types. What do you mean by 'systems programming language'?
- Rusky 13y ago
  The tutorial says "The goal of the IDRIS project is to build a dependently typed language suitable for verifiable systems programming. To this end, IDRIS is a compiled language which aims to generate efficient executable code. It also has a lightweight foreign function interface which allows easy interaction with external C libraries." I generally think of systems programming as drivers, kernels, embedded stuff, and performance-sensitive applications like game engines. Not sure how far in this direction IDRIS is going though. It feels a lot like the same niche as OCaml, with dependent types.
  - edwinb 13y ago
    I tend not to use the phrase "systems programming" any more. "General purpose" is probably better (or my current favourite "Pac-man complete"). I should probably edit the tutorial to that effect. We've done simple network protocols and packet formats (I had a student working on DNS for example) but not driver or kernel level things. That said, some people are experimenting with lower level things (thinking about making a minimal run time system with no garbage collection for example). It's not a primary goal, but it'll be interesting to see what comes of it.
    - bjz_ 13y ago
      > I should probably edit the tutorial to that effect. Yes please do. Idris is a lovely language for bringing dependent types closer to the realm of production code, but giving people false hopes is a little cruel :)
      - tel 13y ago
        Take a look at ATS then! My understanding from playing around with it is it is trying to be C with dependent types.
        thinkpad20 13y ago
        ATS looks fascinating in concept, but what code examples I've seen, the syntax is terrible and it's ridiculously verbose. I'm sure you could write absolutely bulletproof code in it, but the productivity hit would render it almost unusable for large-scale projects. I might be off here, of course... but one of the lovely things about Haskell is that despite its reputation as a difficult language, once certain key concepts are tackled, it's relatively easy to program rapidly and create real world products (with a considerably higher assurance of correctness than most languages provide). ATS seems complex to a level that nearly guarantees its usage won't extend much beyond academia.
        bjz_ 13y ago
        Indeed. I love the idea of ATS, but it seems like it would be a challenge to wrangle with. Whilst Rust isn't a flexible and powerful as ATS, it seems to be much easier to handle at the moment.
        doublec 13y ago
        I think any language you're not familiar can seem like that - especially if it uses unfamiliar sigils or syntax. I feel similar about Rust for example as I'm not as experienced with it. But with ATS I can put programs together pretty quickly - all because I've learnt it.
        bjz_ 13y ago
        Thanks! Yeah, it's hard when you haven't used a language all that much to judge. I wish the sold themselves better though. The website is atrocious for folks wanting to get started with some code. :(
  - bjz_ 13y ago
    'Dependently typed systems programming' was something that really excited me when I first learned of Idris, but it seems that they have backed down from that claim. Indeed, the home page now reads, "Idris is a general purpose pure functional programming language with dependent types".

Dewie 13y ago

> It's cool to see a systems programming language with dependent types. What do you mean by 'systems programming language'?

Rusky 13y ago
The tutorial says "The goal of the IDRIS project is to build a dependently typed language suitable for verifiable systems programming. To this end, IDRIS is a compiled language which aims to generate efficient executable code. It also has a lightweight foreign function interface which allows easy interaction with external C libraries." I generally think of systems programming as drivers, kernels, embedded stuff, and performance-sensitive applications like game engines. Not sure how far in this direction IDRIS is going though. It feels a lot like the same niche as OCaml, with dependent types.
- edwinb 13y ago
  I tend not to use the phrase "systems programming" any more. "General purpose" is probably better (or my current favourite "Pac-man complete"). I should probably edit the tutorial to that effect. We've done simple network protocols and packet formats (I had a student working on DNS for example) but not driver or kernel level things. That said, some people are experimenting with lower level things (thinking about making a minimal run time system with no garbage collection for example). It's not a primary goal, but it'll be interesting to see what comes of it.
  - bjz_ 13y ago
    > I should probably edit the tutorial to that effect. Yes please do. Idris is a lovely language for bringing dependent types closer to the realm of production code, but giving people false hopes is a little cruel :)
    - tel 13y ago
      Take a look at ATS then! My understanding from playing around with it is it is trying to be C with dependent types.
      - thinkpad20 13y ago
        ATS looks fascinating in concept, but what code examples I've seen, the syntax is terrible and it's ridiculously verbose. I'm sure you could write absolutely bulletproof code in it, but the productivity hit would render it almost unusable for large-scale projects. I might be off here, of course... but one of the lovely things about Haskell is that despite its reputation as a difficult language, once certain key concepts are tackled, it's relatively easy to program rapidly and create real world products (with a considerably higher assurance of correctness than most languages provide). ATS seems complex to a level that nearly guarantees its usage won't extend much beyond academia.
        bjz_ 13y ago
        Indeed. I love the idea of ATS, but it seems like it would be a challenge to wrangle with. Whilst Rust isn't a flexible and powerful as ATS, it seems to be much easier to handle at the moment.
        doublec 13y ago
        I think any language you're not familiar can seem like that - especially if it uses unfamiliar sigils or syntax. I feel similar about Rust for example as I'm not as experienced with it. But with ATS I can put programs together pretty quickly - all because I've learnt it.
        bjz_ 13y ago
        Thanks! Yeah, it's hard when you haven't used a language all that much to judge. I wish the sold themselves better though. The website is atrocious for folks wanting to get started with some code. :(
- bjz_ 13y ago
  'Dependently typed systems programming' was something that really excited me when I first learned of Idris, but it seems that they have backed down from that claim. Indeed, the home page now reads, "Idris is a general purpose pure functional programming language with dependent types".