edwinb

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.

There's a tutorial on just this sort of thing here: http://docs.idris-lang.org/en/latest/st/index.html

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

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

That's right.

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

Sorry about that, it's back now...