Hacker News Reader

Comment by Rusky | Hacker News Reader

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.

View on HN

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.

> 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 :)

Take a look at ATS then! My understanding from playing around with it is it is trying to be C with dependent types.

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.

If you use the non-dependently typed parts of ATS it is no more verbose than most ML variants. If you use it without the GC then verbosity increased because you need to add calls to free memory. If you add proofs or dependent types then declaring those adds more. I've used it in moderately sized production programs and it's similar to using OCaml or other ML in terms of productivity. Once you're familiar with the language of course.

If I paraphrase what you said about Haskell it's true for ATS too:

    "but one of the lovely things about ATS 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)."

The key, like any language, is learning the concepts. I think people assume ATS is more difficult than it is is because much of the documentation and examples for it use a verbose style and heavy proofs. A post I wrote a while back attempts to gently introduce ATS dependent types and you can see that the non-dependently typed examples are very similar to any other ML language:

http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.h...

> If you use it without the GC then verbosity increased because you need to add calls to free memory

The issue is that is the default mode I would like to work in. Rust is designed to make that the natural mode of working, rather than the exception. Fast, deterministic operations should be easier and more succinct than the managed alternatives – in the context of a systems language that is.

> people assume ATS is more difficult than it is is because much of the documentation and examples for it use a verbose style and heavy proofs.

Then they need better docs. And a better website! And better marketing!

It's interesting looking at the different design decisions of languages. One persons pro is another's con.

ATS2 has no GC as the default mode of working too. The only reason it is more verbose is because you need the call to free. ATS strives to be explicit in what it does so it's easier to read the code and know what is happening.

Languages with destructors or implicit function calls seem to lean towards the C++ downside of "What does this code really do" when looking at it. I dislike hidden code where there is no easily identifiable call to tell you something is happening.

It's not all roses and unicorns with ATS either of course. What I really want is the next generation of dependently typed system languages which has learnt from the current ones.

> you need the call to free

So how does ATS enforce memory safety? With Rust you have a bunch of library types that you can reuse that abstract away from the memory management for you. The types make sure you don't screw up. Unfortunately you can't prove things about the `unsafe` blocks, and have to rely on careful auditing, but that only needs to be done once, and then you have a nice, reusable abstraction. Bookkeeping sucks.

> What I really want is the next generation of dependently typed system languages which has learnt from the current ones.

Agreed. At the moment Rust suits me the best, but I definitely don't think it is the end of the road.

> So how does ATS enforce memory safety?

Linear types. Much like unique pointers in Rust, the type system tells you when you fail to consume a linear type. A 'free' call would do this. Same with closing files, etc - you use linear types to track that the resource is consumed.

Ah neat. Does it have regions?

And to be clear, ridiculously verbose, dense, and unreadable proofs is the UX failing of most DT languages today. My understanding is that ATS is not significantly better or worse in that department.

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.

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.

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

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

Reply on news.ycombinator.com