Viewing profile — 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…

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 t…

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 som…

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…

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 …

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 …

> 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 nu…

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

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 tu…

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