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…
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…
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…
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.…
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,…
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…
> 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…
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…
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…
Sorry about that, it's back now...
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…
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…
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…
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.…
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,…
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…
> 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…
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…
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…
Sorry about that, it's back now...