3 ms·
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 si
by pathsjs 11y ago
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 11y ago> 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.)