[lomnakkus]

I believe the Idris runtime uses erasure rather than code generation[1]. The key here is that Idris will make call sites prove statically that the conditions hold, either through having static conditions of their own or proving that the programmer has checked (at runtime) that the conditions hold.

(This case of append-n-to-m-vector is a bit weird since it basically just amounts to calculating the length of the output, but my previous statement applies a bit more generally.)

[1] So one plausible representation for Vec n a would be a size + array of pointers to a's. I believe they're actually using linked list for Vec at the moment, though.

[pathsjs]

Yes, but my question is: even if you use erasure, what are you going to do at the call site? Won't you need to state a concrete size there? For usual generic types, erasure and code generation are equivalent in what they can do, because at some point you will specialize to concrete types.

I would be curious to see an Idris program that reads two vectors out of some file (without knowing the size a priori) and concatenates them

[lomnakkus]

> Yes, but my question is: even if you use erasure, what are you going to do at the call site? Won't you need to state a concrete size there?

No, Idris doesn't actually care what "n" and "m" are (concretely)... it just knows that if you happen to have a (Vec n a) and (Vec m a) lying arond, then you'll get a (Vec (n+m) a) out.

> For usual generic types, erasure and code generation are equivalent in what they can do, because at some point you will specialize to concrete types.

I'm not sure I fully understand what you mean, but I think this is slightly wrong... You can think of the fully erased (Vec n a) representation as (n, void-star) in C-style or Array<Object> in JVM style. Note that "a" doesn't actually appear. So the type is actually never needed at runtime -- all functions which have (Vec n a) as a parameter will just assume that it has been (statically) proven[1] that the pointed-to-array has the correct size. Because of parametricity, functions will not be allowed to actually access any 'a' values directly. So it all works out.

Here's another comment of mine that goes a bit deeper into the interplay between static proof and runtime checks: https://news.ycombinator.com/item?id=10302863

Key being: You either need to prove statically or you need to prove statically that you've checked at runtime.

HTH.

[1] This is valid because call sites must provide such a proof (statically).

[pathsjs]

I will try to be more clear. Say the size is actually unknown until runtime, for instance a vector is read from a file.

You cannot apply directly any of the size-aware functions, because it will not typecheck. I only see two avenues:

Either you assert statically that the vector has some concrete size, in which case the size is known statically and the code generation will work as well;

Or you use some other size-unaware function, in which case it is false that Idris can use runtime values as type parameters.

If I understand correctly, you are saying that there is a third possibility, but I am missing it

[lomnakkus]

> I will try to be more clear. Say the size is actually unknown until runtime, for instance a vector is read from a file. You cannot apply directly any of the size-aware functions, because it will not typecheck.

Yes, you can in fact do that! Let's assume you're building the list you're reading from a file as if it were a linked list. That's the point of dependent types -- the types can (and often do) depend on run-time values.

EDIT: I suppose I should expand on this a bit. The idea is that the "read-Vec-from-file" function can look like this:

    readVecFromFile :: File -> (n, Vec n Int)

(let's say it's reading Ints)

So the readVecFromFile function will return you a run-time value "n" (the number of items) and a vector which has that exact length. When using readVecFromFile, you'd do something like

    (n, v) <- readVecFromFile

and you'd be absolutely free to call any function which expects a vector of any length. (If necessary you could also supply the actual length, but that's just a detail.)

The implementation of readVecFromFile is left as an exercise, but it can be done. One idea is to start with the empty vector (length 0) and an "n" of 0 -- and then to just accumulate into it, all the while keeping a "proof" that the length of the vector is way the runtime value says it is. (Using structural induction, basically, to build a proof that the runtime value is the same as the length of the vector.)

[pathsjs]

Ok, I see how it can work. Thank you very much for your explanation!

[lomnakkus]

Actually, I see that I was a bit sloppy in that post wrt. the type annotations and editing, but I'm glad it helped :).