Hacker News Reader

Comment by skrebbel | Hacker News Reader

I love the concept, but the tutorial somewhat puts me off (admission: I only read the first third).

I mean, using an "element from a finite set" to index a vector? Back home, we use natural numbers for that. Idris also has natural numbers, but somehow we still have to, essentially, use the "finite set of values we don't care about, but that we can order if we want to since, after all, the set has a finite number of elements" concept for what's essentially an array lookup.

Why can't there be a type of "natural numbers under N"?

Or am I all misunderstanding things, and is the "finite set" exactly that type, just explained in a very not straight forward way?

Also, impressively, the author claims it has C-style speed. Does that mean that looking up a value in a vector by means of an element in a finite set is actually translated to a single *(vect+index)? (in C-terms)

View on HN

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 set {1, 1, 1, 1} has only one element, 1.

Oh fuck. Bags and sets.

I'm an idiot!

And that only 3 years out of university :-(

I haven't read the tutorial at all, but in dependently typed languages the type (Fin N) is exactly the type of "natural numbers under N", and I expect that is what Edwin is using in the tutorial.

As for compiling to that pointer access: from what I know of Idris, yes it will. Since you know statically that the array access cannot be out of bounds, you can omit the usual out-of-bounds checks.

Reply on news.ycombinator.com