edwinb

3 ms·

1.
by edwinb 8y ago
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 i
2.
by edwinb 10y ago
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 cha
3.
by edwinb 10y ago
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
4.
by edwinb 12y ago
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
5.
by edwinb 12y ago
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
6.
by edwinb 12y ago
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 don
7.
by edwinb 12y ago
> 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
8.
by edwinb 15y ago
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 a
9.
by edwinb 15y ago
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 th
10.
by edwinb 15y ago
Sorry about that, it's back now...