Conversation
.devcontainer/devcontainer.json
Outdated
| @@ -0,0 +1,20 @@ | |||
| { | |||
There was a problem hiding this comment.
any reason to add this file?
There was a problem hiding this comment.
Oh sorry, I should have explained. This was so I could develop the project on GitHub Codespaces (instead of using more disk space on my laptop). It's up to you if you want to merge it in or not, I can remove it from any future mergeable PRs. It's actually not foolproof because it doesn't install Stack by default yet. If you're interested I'll get it fully working, if not, I'll leave it as-is/remove it before we merge.
There was a problem hiding this comment.
I'm not against this, but I'm hesitant to say we should merge until (at least):
- We've cleaned up our own project configuration a little bit.
- We can install all dependencies (for which we have many) through the file.
- We write instructions on how to use it.
- We confirm that it works for all of usual tasks and that we have a usecase. The pricing of Codespaces doesn't look too bad, which is certainly appealing if we ever have students with low-spec computers!
Does HLS work with this? I would imagine that GitHub Codespaces has fairly limited resources?
There was a problem hiding this comment.
So we should definitely not merge this in via this particular PR.
There was a problem hiding this comment.
@balacij HLS works on Codespaces just fine, the smallest one has 2 vCores, 8gb of RAM and 32gb of storage. But I agree we shouldn't merge this yet.
There was a problem hiding this comment.
Also, there is a way to get "unlimited" (for practical purposes) Codespaces for free for education settings. It is nice for helping people get started for sure.
|
As to your questions:
|
|
@JacquesCarette Thanks, I'll get to work on those things! So, representing matrices as arrays makes sense, and it along the lines of what you're already doing. I guess what I'm still not sure about is how we unify the idea of clifs and arrays (since matrices can be represented as arrays)? How we represent a vector is pretty obvious: it's a vector (grade-1) clif. But how do we represent multi-dimensional arrays (and therefore, matrices) as clifs? Or do we keep around the idea of arrays? But that feels weird because I was under the impression that we're trying to unify the whole understanding of vectors/matrices/etc under Clifford/geometric algebra. |
|
Arrays already exist -- in the backend. They are "implementation structures". We don't need to talk about them at the theory / specification stage. If you start trying to implement vectors (and just vectors, but as clifs) and try to push them through the whole codebase, I think it will all become much clearer. Let Haskell lead you to where things break. Pithy motto: vectors (clifs) in the math, arrays in the CS. Drasil's pipeline actively transforms math to CS. |
|
The latest commit is a nice way to track down everything that needs to be touched. |
Thanks, my plan is to try to get it all ported over to the new exprs/"shapes" and have it compile. I just committed what I had when I stopped last night to "save" it even though it doesn't currently compile. |
|
Finished doing a bunch of refactoring. In addition to looking at it, I had some questions (some of which correspond to TODOs in the code):
|
| (customClass [constructorInfo odeCtor [] [], | ||
| methodInfoNoReturn odeOp "function representation of ODE system" | ||
| [unnamedParam (Vect Real), unnamedParam (Vect Real), lockedParam t] | ||
| [unnamedParam undefined, unnamedParam undefined, lockedParam t] -- TODO: what do we put here? We need specific dimensions now. |
There was a problem hiding this comment.
Design decision needs to be made: either we support "arbitrary" dimensional vector spaces (i.e. where the dimension is not mentioned" or we support "specific but unknown" (i.e. symbolic) dimension. Or both.
There was a problem hiding this comment.
Yes. Currently, I support specific dimensions and symbolic dimensions (currently, very simple ones: strings). We could add more such as "dimension is not mentioned" (not sure the ramifications of that for the operations), and things like addition of dimensions.
There was a problem hiding this comment.
Let's try to handle this particular case with symbolic dimensions and see what that means, i.e. what else that forces us to think about.
| spaceToCodeType S.String = [String] | ||
| spaceToCodeType (S.Vect s) = map List (spaceToCodeType s) | ||
| spaceToCodeType (S.ClifS _ _ s) = map List (spaceToCodeType s) | ||
| spaceToCodeType (S.Matrix _ _ s) = map (List . List) (spaceToCodeType s) |
There was a problem hiding this comment.
I guess you're choosing not to replace Matrix with ClifS this go around?
There was a problem hiding this comment.
Oops - I should have included that as another question. I didn't because I wasn't quite sure what kind of clif it should be represented as. Do you have thoughts? Would an m-by-n matrix be represented as something like an n-grade clif in an m-dimensional space? Dr. Smith and I did some research and there's not much about using clifs to represent matrices. The geometric algebra people have this attitude of "we don't need matrices" so they seem not to even think about them.
There was a problem hiding this comment.
https://math.stackexchange.com/questions/850869/linear-algebra-without-matrices is one place to start reading. It points to the nice book "Linear Algebra Done Right" which is really quite a gem. [In a sense, chapter 1 of https://arkadiusz-jadczyk.eu/docs/clifford.pdf says that concrete Clifford Algebras are equivalent to some spaces of matrices...]
However, we will still want to be able to enter 'concrete' matrices (in a basis).
The book "Guide to Geometric Algebra in Practice " is available for download from McMaster's library - I think that one would help most.
There was a problem hiding this comment.
@JacquesCarette these look to be good resources. @CSchank can you please add links to these resources to your slide show on Clifford algebra. I worry that if we the links only appear here, we won't be able to find them in the future if we go looking. 😄
code/drasil-code/lib/Language/Drasil/Code/Imperative/ReadInput.hs
Outdated
Show resolved
Hide resolved
| -- | Gets the dimension of a 'Space'. | ||
| getDimension :: Space -> Int | ||
| getDimension (Vect t) = 1 + getDimension t | ||
| getDimension (ClifS _ _ s) = 1 + getDimension s -- TODO: Does this make sense? Maybe we're overloading the term "dimension" now. |
There was a problem hiding this comment.
I agree, this is weird. Can you figure out who calls getDimension and what they need from it? It looks like this is always going to return '1' for a Vector and 0 in all other cases!
There was a problem hiding this comment.
Well, we had things like Vect (Vect Natural) which would return 2.
There was a problem hiding this comment.
Ah, yes. Horrible hack that. See if you can get rid of it?
| -- | Converts a list of 'String's to a Matrix 'Expr' of a given 'Space'. | ||
| -- | Converts a list of 'String's to a Clif 'Expr' of a given 'Space'. | ||
| strListAsExpr :: Space -> [String] -> Expr | ||
| strListAsExpr (Vect t) ss = Matrix [map (strAsExpr t) ss] |
There was a problem hiding this comment.
you shouldn't do Matrix partially; either try for all cases or none, but not just some!
| -- | Converts a 2D list of 'String's to a Clif 'Expr' of a given 'Space'. | ||
| strList2DAsExpr :: Space -> [[String]] -> Expr | ||
| strList2DAsExpr (Vect (Vect t)) sss = Matrix $ map (map (strAsExpr t)) sss | ||
| strList2DAsExpr (ClifS gr0 d0 (ClifS gr1 d1 s)) sss = undefined -- TODO: fill this in |
There was a problem hiding this comment.
Trying to fill these particular TODOs will be very instructive.
There was a problem hiding this comment.
This is another question I had: does geometric algebra have such a thing as "clifs of clifs"?
There was a problem hiding this comment.
Didn't think so. So, if Clifs take Expr as an argument, we will have to have type checking to make sure they don't take another clif as an argument.
| extractColumnCT :: Func | ||
| extractColumnCT = funcDef "extractColumn" "Extracts a column from a 2D matrix" | ||
| [mat, j] (Vect Real) (Just "column of the given matrix at the given index") | ||
| [mat, j] (vect3D Real) (Just "column of the given matrix at the given index") -- TODO: is this correct? |
There was a problem hiding this comment.
while the above 3Ds are likely right, I agree, this one is less clear. You'll have to see where extractColumnCT is used to see what the context says.
There was a problem hiding this comment.
Yeah, so this is to extract a given column in the matrix. It's used as part of this:
interpMod :: Mod
interpMod = packmod "Interpolation"
"Provides functions for linear interpolation on three-dimensional data" []
[linInterpCT, findCT, extractColumnCT, interpY, interpZ]So yes, 3D.
There was a problem hiding this comment.
Right, so this is 'different' in the sense that this isn't a semantic operation but rather this is a programming-level operation where an array is used for packed storage and then its columns are extracted.
So in a separate language (ModelExpr ?), we need ways to talk about storage and concrete representations. It's a typical mistake to conflate these.
There was a problem hiding this comment.
@JacquesCarette should this separate language be within the scope of the project by @CSchank? Ideally I would like us to include at least parts of this other language as needed for the current examples, but I don't have a feel for how difficult a task this is.
There was a problem hiding this comment.
It should be in-scope. It's a much simpler language.
| (nounPhraseSP "temperature of the water") | ||
| "the average kinetic energy of the particles within the water" | ||
| (sub (eqSymb temp) lWater) centigrade (Vect Real) | ||
| (sub (eqSymb temp) lWater) centigrade (vect undefined Real) -- TODO: dimension of vector? |
There was a problem hiding this comment.
I'm having trouble thinking of what the dimension of tempW should be. The temperature of the water is a scalar value. The problem is 1D. There is only one temperature for the water. It varies over time, but not over space. Even if temperature varies over space, it is still a scalar. The only reason I can think for a vector is that in solving the ODE we use a vector, but Tw is one of the components of the vector, not a vector itself.
There was a problem hiding this comment.
So this is a bug in our 'formalization' of tempW?
There was a problem hiding this comment.
I don't know if it is a bug, or a misunderstanding on my part. The generated documentation for tempW has been reviewed many times, so I believe it is correct. The definition of tempW looks good (the average kinetic energy part) and I believe that part appears in the generated documentation. I don't know if the type of tempW is ever displayed or used. If the "formalization" of tempW is not used to do anything, it could be wrong and we'd never know because there are no consequences of a mistake. If someone could explain the consequences of the formalization in the generated artifacts, I would help judge whether they are correct or not. If they really aren't used, then I'm fairly sure they are currently incorrect. 😄
There was a problem hiding this comment.
I'm not sure we print 'types' in the SRS (because they didn't exist when you last reviewed). So I wouldn't be surprised if there were uncaught bugs here.
There was a problem hiding this comment.
I'm fine with using Real for Tw just to move on, but the constraint isn't on a single value of Tw; it is on every value of the function for Tw between the start of the simulation and the conclusion of the simulation. The constraint should be something like:
Since we don't handle types consistently right now, I don't think we should make any changes. It also seems out of scope of the work by @CSchank to explore this. 😄
There was a problem hiding this comment.
@smiths well, I now have a partial answer why this was listed as a vector type. I tried running the example again changed to Real and I got an error produced by this line of code, producing the following error:
=====[ Start type checking ]=====
`theory:eBalanceOnWtrRC` exposes ill-typed expressions!
- ERROR: Associative arithmetic operation expects all operands to be of the same expected type.
Received:
- ERROR: List accessor expects a list/vector, but received `Real`.
`heatEInWtrIM` exposes ill-typed expressions!
- ERROR: Associative arithmetic operation expects all operands to be of the same expected type.
Received:
- Real
- ERROR: Function application on non-function `tempW` (Real).
`wMass` OK!
`wVol` OK!
`tankVol` OK!
`tauW` OK!
=====[ Finished type checking ]=====
swhsnopcm: Type mismatch between variable and value in declare-define FuncStmt
CallStack (from HasCallStack):
error, called at lib/Language/Drasil/Code/Imperative/Import.hs:650:28 in drasil-code-0.1.9.0-BZ5f3ZI9HUq1TjClKZN633:Language.Drasil.Code.Imperative.Import
From what I can understand from that linked line of code, this section of the code checks an expression that is a function definition to ensure that if the output type is a matrix then the input type must be either a list or an array. At some point vectors (now clifs) get converted into arrays for their concrete code representation. Reals, of course, do not get converted to arrays or lists. So this caused this error. So obviously this type is factoring in, albeit in a pretty roundabout way. So I'll have to switch it back to vectND (a clif) for now to appease avoid this error for now as, like you said, this issue is beyond my scope.
There was a problem hiding this comment.
Thank you for the explanation @CSchank. I agree with your solution. In some sense, it is a good error. The generated code will not be a single scalar for the output. The types of the output in the code and the output in the SRS should be the same, or at least have a translation between them, like between a continuous function and a discrete sequence of output. Since we don't have types fully and consistently used right now, we should move on from this instance and let it be sorted out in the future when types are handled more consistently and completely.
There was a problem hiding this comment.
Sounds good, thank you!
|
The type checking errors is because... things are currently broken! Our use of vectors is quite bad, i.e. type incorrect. And there was no point in fixing it in the current state. We will indeed encounter even worse bugs. Like you have in For the other things you ask, I left comments in the PR itself so that they are 'in context'. The way you asked with insufficient context made it impossible for me to understand what the questions really were. |
|
|
||
| acceleration = uc CP.acceleration (Concat [vec lA, label "(", lT, label ")"]) (Vect Real) accelU | ||
| -- TODO: what should the type here be? | ||
| acceleration = uc CP.acceleration (Concat [vec lA, label "(", lT, label ")"]) undefined accelU |
There was a problem hiding this comment.
Taking a look at usage in GamePhysics, a Real -> Real function seems more likely than a Vect Real.
There was a problem hiding this comment.
Note that functions are still mostly unsupported as well, hence why the time variable is manually added to the symbol of acceleration.
There was a problem hiding this comment.
Another option for the type is Real -> Vect Real. In 3D the acceleration is a function of time. In general, at any time, we can have 3 components of acceleration. We also have a 1D version of acceleration in Game Physics which would have the type Real -> Real.
There was a problem hiding this comment.
This is a symptom of a deeper problem in Drasil: acceleration should exist in many different ways (as a concept, as an instance of properties for several objects, but also as something that may be represented in different ways!)
So acceleration can be Real, Vect Real and Real -> Real depending on the case at hand. Thus we need to be able to do that.
There was a problem hiding this comment.
So this is where @CSchank is likely going to need to rely on @balacij sorting out some stuff in our chunks.
For this one: I don't think the concept of acceleration should be a UnitalChunk because its 'units' will actually depend on the setting in which it is used, i.e. acceleration gets a unit once the object of concern is known.
We could treat it as a vector of unknown dimension if we insisted on giving it units 'early', thus indicating that it is a dependent concept.
There was a problem hiding this comment.
@balacij any chance we can work on this?
There was a problem hiding this comment.
@balacij might now be free, given that his Comp II was earlier today.
There was a problem hiding this comment.
Hi, sorry @CSchank! I will message you on Discord!
|
Out of curiosity, which resources are we using to pull this from? I'm unfamiliar with Clifford algebra and would like to learn more so I can help too. Also, assuming you're still designing the Clif data type, it might be worth implementing a prototype externally first (because Drasil can be difficult to work with) with:
Afterwards, you can:
Afterwhich, we can figure out how Drasil needs to be pushed around to implement the Clifford algebra and have the Clif code generation work. If you chose to do this, nothing in this PR would be lost. (I mention this in part because I intend to soon edit nearby pieces of code, so I want to avoid merge conflicts as much as possible.) |
|
@balacij you can learn more about Clifford Algebra from Chris's SRS slides. The slides cite a good introduction to Clifford Algebra. An external prototype is an idea that is definitely worth thinking about. |
|
While I agree that working directly in Drasil is difficult, shaking out the design will only be possible within the full Drasil. Until it proves too difficult, I think it best to stay the current course. |
ptrandev
left a comment
There was a problem hiding this comment.
Coming from CSchank/GeometricCodeGen#13
I'm a relative novice with Haskell, but adding feedback to strengthen the conceptual understanding of what this PR is achieving.
code/drasil-code/lib/Language/Drasil/Code/Imperative/ReadInput.hs
Outdated
Show resolved
Hide resolved
| UnaryOpVN :: UFuncVN -> Expr -> Expr | ||
| -- | Unary operation for @Clif -> Clif@ operations. | ||
| UnaryOpCC :: UFuncCC -> Expr -> Expr | ||
| -- | Unary operation for @Clif -> Clif@ operations. |
There was a problem hiding this comment.
You may need to update the comment here. I believe this is converting @Clif -> Number@, not @Clif to Clif@
|
The other day I:
This raised some questions we have to answer:
|
|
@CSchank great to see this pull request. It looks like the generated version does not match stable and that the linter failed. Can you please look into these CI problems? If you need help, we can possibly enlist the summer research assistants. |
|
Hi @JacquesCarette, @balacij, @smiths, et al. I believe this PR is ready for review. The goal of this PR is to replace vectors with the geometric algebra (clif) constructor/space. It looks like there are some differences in some of the examples, but I don't believe I caused them? Please look them over and let me know. This currently has a few limitations:
|
|
Unfortunately we hadn't met yesterday -- my fault! We're going to meet this afternoon to discuss it. |
|
Sounds good @balacij. |
| (customClass [constructorInfo odeCtor [] [], | ||
| methodInfoNoReturn odeOp "function representation of ODE system" | ||
| [unnamedParam (Vect Real), unnamedParam (Vect Real), lockedParam t] | ||
| [unnamedParam (vectNDS "n" Real), unnamedParam (vectNDS "n" Real), lockedParam t] -- TODO: what do we put here? We need specific dimensions now. |
There was a problem hiding this comment.
@CSchank Do you think you could give an example please? Of the change you'd like to see, that is.
There was a problem hiding this comment.
Shouldn't we specify the dimension in each example to match its requirements? So here it must remain abstract?
| mapWithIndex :: (Natural -> a -> b) -> [a] -> [b] | ||
| mapWithIndex f xs = | ||
| mapWithIndex' 0 xs | ||
| where | ||
| mapWithIndex' _ [] = [] | ||
| mapWithIndex' n (x:xs) = | ||
| f n x : mapWithIndex' (n+1) xs |
There was a problem hiding this comment.
Needs to be moved to drasil-utils.
|
Linear and Geometric Algebra might help us out with the matrix issue. I just need to find us a copy now. Some related projects that might be helpful:
|
|
That does look like a good book @balacij. I searched the table of contents, introduction and index and the word matrix comes up many times. The author says that matrices are not as important in geometric algebra, but he still covers the topic. I'm optimistic that he would make the connection between traditional and geometric algebra. It would be great to find a copy that has the middle chapters, and not just the first few and last few pages. 😄 It is unlikely, but our library might have a copy, or be able to get it through interlibrary loan. |
| Void :: Space | ||
| -- | Clifford algebra objects (Clifs) with a dimension | ||
| -- TODO: Can this be just called `Clif`, depsite shadowing the binding in `*Expr`, since we `import qualified Space as S` usually? | ||
| ClifS :: Dimension -> Space -> Space |
There was a problem hiding this comment.
type Field = Space^ To indicate that the Space needs to be a field. We can upgrade it later or do that now too with a newtype, or ... etc.
@JacquesCarette Can you help us (@sarrasoussia and I) clarify some things?
- Name: Multivectors? Should the name of this type be
ClifS? Or is it the type of multivectors? A multivector is the type of the objects that live within the "ClifS", which is really what we want to talk about with expressions of this type. - Dimension:
ClifScontains anIntfor the "dimension" -- is this the related to the term which has the most "wedged" number of vectors together (@CSchank -- e.g., 3 for an expression that adds a scalar, vector, and trivector)? Or is this the dimension of the vectors? Should we have both (@JacquesCarette)? Assuming we carry the dimension of the clifford algebra: should we carry positive and negative dimension separately in the type of "ClifS"/Multivectors? Terminology surrounding "dimension" is a bit overloaded here. I hope dimension is related to the number of components in the vectors of the related vector space. - Types: Assuming we are going to have a multivector type, should we also have the type of "big wedge"? e.g.,
BigWedge :: Int -> Space. Though, what is the actual name? "Exterior Power"? - More Types:
ClifScould be interpreted as the type signature of a vector as well. But assumingClifShere really means "multivector", then this is a very different thing than a "vector". A Multivector can have a bivector component, trivector component, scalar, etc... a 'vector' cannot. Shouldn't we still have a pure Vector type as well? - Type checking: a vector is a vector, but if we blur the lines, it could be interpreted as a multivector with all other components "set to 0" (@JacquesCarette can you clarify the nomenclature here?). This also applies to Exterior power 1 <=> Vectors, Exterior Power 2 <=> Bivectors, etc. We should probably make the bidirectional type checker actually do something more intensive here to permit this situation. Note to self for this.
There was a problem hiding this comment.
- I don't have a strong opinion on the name. It might be premature to change it until we fully settle on what we're representing.
- If my understanding is correct, we need a "dimension" and a way to represent what is there at each dimension. Yes, it is the number of components of the formal sum.
- No, I don't think so. And, even if we did,
BigWedgewould have to contain more data than that.BigWedgeis a type-former over vector spaces. We don't want to manipulate these 'raw', instead this should be baked into the type forClifs(or whatever it will be called) Clifsat a particular dimension (one), with a particular signature (no component of grade 0) are vectors. So we shouldn't need vectors are they are a special case. We do need the signature part ofClifsto be known data to be able to recognize vectors 'statically'.- Yes, type-checking will need to learn about all of this. That's why the signature part will have to be static, else type-checking will be impossible.
| -- TODO: Fix this to be more specific to Clifs | ||
| -- TODO: How do we control whether to print all the components or just a subset (e.g. only the vector components)? | ||
| modelExpr (Clif _ es) sm = P.Mtx [map (`modelExpr` sm) $ Map.elems es] | ||
| modelExpr (Clif _ es) sm = P.Mtx $ map ((:[]) . (`modelExpr` sm)) $ Map.elems es |
There was a problem hiding this comment.
It looks like the issue was a misunderstanding in how Mtx is supposed to be used. Rows vs columns. A single inner list is a single row in the matrix. However, we seem to want column vectors appearing, so we need multiple rows, only 1 column (i.e., many one-element inner lists).
I think this approach only works for existing case studies, however (in general, i.e., using a matrix here). If one of the basis blades were
There was a problem hiding this comment.
This fix is an improvement, thanks for tracking down this bug.
…is blades when rendering
| -- | Simple ordered map. Based on 'container's 'Data.Map'. Note: Deletions are | ||
| -- unsupported. | ||
| newtype OrderedMap k v = OM { im :: M.Map k (Int, v) } | ||
| deriving (Show, Eq) |
There was a problem hiding this comment.
I just wrote this instead of using an external library. I think we have something similar in our ChunkDB -- though I don't remember why we need to recall order of insertion of things into the ChunkDB, but if this is merged, we can use this one as well.
This was necessary for the rendering of basis blades to be done in order of insertion.

Hi Dr. @JacquesCarette,
I was hoping you could give me some feedback on what I have so far. It's definitely far from complete, this is not really meant to be merged as-is but is a very early WIP. I have not actually removed anything yet, just started to build up what I hope is the right infrastructure to internally represent clifs. I'm hoping you can tell me if I'm on the right track and answer some questions:
Exprconstructors directly instead of their own type?Exprvalues instead ofClifvalues?NGradeCand not have the others (likeVector,Bivector, etc)? Dr. Smith thought we maybe should have the "usual" cases, but those could be smart constructors.module Language.Drasil.Expr.Class.Spaces, should Clifford spaces be able to take in otherSpacevalues, like you've done for these:Set Space | Matrix Int Int Space | Array Space?Vector -> Vector, how do we represent these in the currentExpr, or do I need more constructors?UnaryOpVV) in it with clifs instead of vectors.