There are various reasons why Idris is slow, but it generally comes down to it being because the current system is the result of lots of experimentation about how to even implement a dependently typed language in the first place, and what it should look like. It needs quite a bit of re-engineering - I prioritised ease of playing with features over efficiency.
The good news is that I'm working on a new version, taking into account the many things I know now that I didn't when starting on version 1. Don't hold your breath though, it might take a while...
In the end, it's a research project, and our job isn't so much to make a good product as to get people excited about the ideas. Mostly we do this by trying to be obviously having lots of fun. But I'd still like a better implementation, because then we can have even more fun.
Tracking state (sort of like Typestate) is not part of the type system, but you can encode it in the type system. So far, I've found this much more usable in practice than linear types, but I expect future work on linear types will change this, especially now that they're coming to GHC.
The new States library is really a new implementation of Effects. It works in pretty much the same way, but emphasising the thing that the Effects library is best at and fixing some of its shortcomings.
There are two main differences at the moment:
- Everything has to be labelled
- There's no 'implicit' lifting of smaller sets of states
The first is annoying for things like Console IO, so I might change that. The second means that we have a much better chance of providing decent error messages, one day.
As I see it, this is not so much a book at this stage as an introductory tutorial written by someone as they were learning Agda (about four years ago I think), as a contribution to the community to help other beginners. As such, one of the (unstated) assumptions is that the reader is already motivated to learn about programming with dependent types.
The early examples you see with inductive structures such as Nat are about learning the foundations, and you can't go on to do anything especially interesting without a solid understanding of the foundations. Its structure often also turns out to have a convenient correspondence with more realistic data structures, such as lists (their length) and trees (their depth).
I do sometimes wonder if we should start using something more obviously useful as an introductory example though. There's plenty of possibilities, and programmers aren't generally going to be using Nats in practice (I rarely do).
I don't use Agda myself (I use Idris, which is similar but is more directly aimed at general purpose programming) but I do know that it has primitive types...
Anyway, there's all kinds of interesting work going on at the minute which goes way beyond these introductory examples. For example, we're working on a way of specifying and verifying implementations of communication protocols (https://github.com/edwinb/Protocols), which we'd like to apply to cryptographic protocols when we've made some more progress. You can hear me waffling on about that, as well as about how we deal with stateful systems in general, here: https://www.youtube.com/watch?v=rXXn4UunOkE&feature=youtu.be
I post this mainly because I suspect I'm one of the wonks who was researching dependently typed programming at your university ten years ago. At the time, there was lots of foundational work to do, and there is still lots to do before it's industrial strength, but we've made a lot of progress, and I think the goal is worth striving for.
It's hard to write something that's generic over a uniqueness type and a normal type, which is indeed a bit of a pain. It's not completely impossible: we have a kind 'Type*' which covers both unique and normal types, which can be used to make some polymorphic functions which preserve uniqueness, but that's all at the minute.
On the other hand, I see them as something you use when you want more precise control over memory management, control of in-place update and so on.
As ever, there's a trade off between efficiency and abstraction, which is where the partial evaluator comes in. This is still experimental and we're working on it, but I'm wondering if we can use partial evaluation to turn nicely abstract high level code into something efficient based on uniqueness types at run time.
I guess my main worry with this scheme would be fragmentation, having 3rd party libraries not bothering using Type* where it makes sense and making it very difficult to write code using uniqueness types. I guess I'll have to learn me some Idris and see for myself, the language looks very interesting.
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 :)
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:
> 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.
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.
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.
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. :(
> It would be, but the compiler recognizes the pattern and does ordinary integer arithmetic where it needs to (the pattern is relevant, however, to the use of individual natural numbers in defining other types, which is pretty important to Idris.)
The compiler does recognise it, because it'd be silly not to, but more importantly, Nats tend to be type level things which explain the structure of something else (e.g. a successor corresponds to a cons, or to another level in a tree), and as such don't appear in runtime code anyway. If what you want is machine arithmetic, better to use a type that's designed for that.
Idris has Haskell-like syntax because I like Haskell style syntax (this is probably the most important reason!) and Haskell programmers are the initial target audience.
I recently stumbled on something called "view", a concept implemented in the Hope language. For those not familiar with it, it let you define bijections between 2 different datatypes, so that one may pattern match a piece of data from one datatype with the other datatype constructors, and one of the examples in the paper was precisely that correspondence between peano numbers and usual (unsigned) integers (well, really, it's not quite bijective, given the arch limits on integer representation, but for any purposes we can think of yet, it works). So, the question is: is idris using something like that? Or is there another mechanism? Is it a builtin feature of the language? Do you use the proof system to persuade the language kernel it may translate them back and forth (the "software foundation" book for Coq let the reader build a few proofs about that, though Coq use arbitrary precision numbers iirc))? I'm still quite new on dependent typing, so forgive me if this question is silly or weird somehow.
You don't normally need to write each vector function both ways. If you can statically know the length (which you normally do in practice, at least in my experience) then you can write down a more precise type. filter serves as an example of what you might do when you need to compute an index dynamically.
That is indeed exactly what Fin is. The first n natural numbers is a finite set of n elements after all. I'll elaborate a bit in the tutorial. I guess the trouble with writing a tutorial when you're completely familiar with a language is that it's hard to know what will and won't make sense!
There'd also be nothing wrong to use a natural number, along with a proof that it's bounded by the length, to index the vector.
I don't think I've claimed it has C-style speed anywhere. At least, not in general - we have observed it in some cases though, and it is a goal to make it as efficient as possible. Dependent types plus partial evaluation gives you some nice opportunities for optimisation. Early days yet...
That is indeed exactly what Fin is. The first n natural numbers is a finite set of n elements after all.
Ah, right! I must admit that it feels like an odd definition to me indeed. I see how "the first n natural numbers" is a finite set of n elements, but I don't see how the reverse is true. I mean, look here, a finite set of n elements: {1, 1, 1, 1}. 4 elements, and they're all valued 1. They're also not ordered. So your concept of taking an element from a finite set (in this case, let's say, 1, or maybe 1 instead) to uniquely identify an element in a vector sounds a bit odd to me :-)
Clearly, I'm the noob here, and maybe in this stage Idris just isn't meant for people not on Lambda the Ultimate, but if not, it's good that you intend do something about it :-)
Cause once again, I love the concept, and I'd love to program with this.
The good news is that I'm working on a new version, taking into account the many things I know now that I didn't when starting on version 1. Don't hold your breath though, it might take a while...
In the end, it's a research project, and our job isn't so much to make a good product as to get people excited about the ideas. Mostly we do this by trying to be obviously having lots of fun. But I'd still like a better implementation, because then we can have even more fun.