Drasil
Drasil copied to clipboard
JacquesCarette
Specifying size of `Space`'s `Vector`, `Matrix`, and `Array`
Related to #3093
When I think of a "vector", I typically think of something with a known, static, length. Do we want to add vector length to the type signature of vectors?
Of course, we might have an area that creates vectors of a desired length, which might mean that we deal with vectors of unknown length at compiled-artifact-runtime.
EDIT: "we need to make sure that both vectors and matrices can have a static or dynamic size." (from this comment)
EDIT 2: this should also be done for arrays (see this comment)
Yes, the difficulty here is that we might not know it statically.
What we could do is to have vectors know their length, but have typechecking only error out if it gets things like "2 == 3" (i.e. static dimensions clash) and pass through anything that contains symbols. [We could put out diagnostic information, on demand, on what correctness conditions we're assuming are true]
I agree that we won't always know the vector length at specification time. Although we will know the dimension of a force vector, position vector etc in a given space, there are cases where the length won't be known until run time. For instance, if we build a sequence of temperatures over a time discretization (t0, t1, t2, ...), the number of discrete values may be an input that we don't know until run time. I'm sure you could use tricks with staging to know this information before the code is executed, but in a regular scientific program, the step size wouldn't be fixed at the requirements (SRS) stage.
I like the idea of checking the size if we know the size but allowing for cases where we don't know it yet. Seems like a nice and clean solution to me.
Perfect! I will try to play around with this, but it shouldn't be blocking for #3093.
What's the status of this? It seems to be blocking samm82#44. If we constrain the dimensions to integers, the type for compound could be represented as $\mathbb{N}^{118}$; otherwise, if we make it more flexible, it could be represented as $\mathbb{N}^{|E|}$.
I like $\mathbb{N}^{|E|}$ better. It is self-documenting because the reader doesn't need to figure out where the 118 came from. Also, if they discover a new element, it is still correct. :smile:
Just a note that I've been working in this on the lengthForVectMat branch, testing it on my fork in the compDefAsVector branch. I'm able to store the dimension of a vector as an integer, but would like to store it as an expression ($|E|$)
Can you show me (maybe by linking lines in a comment here) how you're going about the implementation? I have ideas on how to potentially do this.
Note that I haven't touched Array yet
This is how I've implemented the dimensions for the spaces themselves:
https://github.com/JacquesCarette/Drasil/blob/5ef55a46ccc6eb90f7805f00a5802b6be4bf4b34/code/drasil-lang/lib/Language/Drasil/Space.hs#L39-L41
and here's how I've implemented printing their dimensions in the SRS:
https://github.com/JacquesCarette/Drasil/blob/5ef55a46ccc6eb90f7805f00a5802b6be4bf4b34/code/drasil-printers/lib/Language/Drasil/Printing/Import/Space.hs#L23-L27
I realize this is an imperfect solution (what if we want a 3D matrix?) but figured it was a good place to start. My next step was to use Exprs to define these dimensions in general terms (as discussed above), but I'm wondering if we should be looking at the code generation side of things first (especially in light of #3504).
Let's stick to 1D and 2D for now.
I would be tempted to do
data StagedInt = Static Int | Symbolic Expr
and use Maybe StagedInt. That would let you have 'symbolic' dimensions that could be typechecked to represent an Int.
That's just complex enough that you might not want to inline the printing put have a separate function.