JacquesCarette
Quasi-Types
Spin-off of Note 3 of https://github.com/JacquesCarette/Drasil/issues/4064#issuecomment-2887572656
Objective
In GlassBR, I believe there are two variables that involve quasi-types, without this being explicitly captured. The goal of this issue is to capture said information and use said information to automatically produce constraints (hidden from the SRS) on quantities.
Background
Pulling from the table of symbols from the live, generated SRS at time of writing:
- $t$: Nominal thickness t is in {2.5,2.7,3.0,4.0,5.0,6.0,8.0,10.0,12.0,16.0,19.0,22.0}
- $g$: Glass type
Additionally noting point 11 from the "Terminology and Definitions" section:
Glass type factor (GTF) - A multiplying factor for adjusting the LR of different glass type, that is, AN, FT, or HS, in monolithic glass, LG (Laminated Glass), or IG (Insulating Glass) constructions.
Both $t$ and $GTF$ are examples of quantities that involve quasi-types.
Quasi-Types
First, an example: $\mathbb{Z}^+$. We define $\mathbb{Z}^+$ as "any value of $\mathbb{Z}$ greater than 0," where $\mathbb{Z}$ is the type of integers. Strictly speaking, members of $\mathbb{Z}^+$ are not of type $\mathbb{Z}^+$, but of $\mathbb{Z}$. $\mathbb{Z}^+$ is only a set of values of type $\mathbb{Z}$. It is only by convention that we might say members of $\mathbb{Z}^+$ are of type $\mathbb{Z}^+$.
A quasi-type is a set of values that acts like a type, but is really a set of values of another type. This quasi-type can be defined by either an enumerated set of values of another type or by a predicate on values of another type. For example, we can define $\mathbb{Z}^{+, \le 10}$ with either $\set{1,2,3,4,5,6,7,8,9,10}$ or $\set{z | z~:~\mathbb{Z}, 0 \lt z \le 10}$. Either way, $\mathbb{Z}^{+, \le 10}$ is a set that acts like a subtype of $\mathbb{Z}$ and whose members are strictly of type $\mathbb{Z}$ but that we might claim to be of type $\mathbb{Z}^{+, \le 10}$.
What does this mean for $t$ and $g$?
Strictly speaking, $t$ is a rational number (according to the Haskell code snippet below, but it could equally be a real number) and $g$ is a string. However, we really want $g$ to be one of $\set{AN, FT, HS}$ and $t$ to be one of $\set{2.5,2.7,3.0,4.0,5.0,6.0,8.0,10.0,12.0,16.0,19.0,22.0}$. Both of these sets are examples of quasi-types. We should capture this information.
Why capture this information?
We have these two constraints that are generated by the code:
https://github.com/JacquesCarette/Drasil/blob/196370e5a3ca95d9be69f9155f6c664dda897f5a/code/stable/glassbr/src/python/InputParameters.py#L216-L241
This is good. However, we do this by writing constraints on the quantities with no clear explanation about why (in the code):
https://github.com/JacquesCarette/Drasil/blob/196370e5a3ca95d9be69f9155f6c664dda897f5a/code/drasil-example/glassbr/lib/Drasil/GlassBR/Unitals.hs#L106-L112
Coincidentally, these two constraints do not appear in the input data constraints table. If constraints were properly automatically found and injected into this table (#4078), then these constraints would appear. However, I'm not so sure they are worth including/should be included in this table. If we had $n > 3$ quantities of a quasi-type, then the constraints table would be polluted with something that should be either implicit through another section or that should be aggregated and recorded differently (i.e., without the excessive repetition). Additionally, in the code, we would need to repeat this constraint $n$ times!
So what should we do?
We should:
- Capture information about quasi-types. This should be done with a chunk that records this.
- Generate the constraints automatically for the variables belonging to quasi-types.
I would say either "defined types" or "enumerated types". In either case, it involves user-defined types. Quasi-types sounds too mystical...
We define Z^+ as "any value of Z greater than 0," where Z is the type of integers. Strictly speaking, members of Z^+ are not of type Z + , but of Z
This is something I've given a lot of thought about lately. So I see this somewhat differently. We need to differentiate between
- semantic types, i.e. the types of things we actually want to model, talk about
- representation types, i.e. the actual representation we use.
For example, Haskell gives us newtype as a feature that helps programmer separate semantic from representation types. Thinking about the 'representation type' is premature optimization, in a way.
In this case, Z^+ is what we want, Z is what we have to settle for because we have no other choice.
Regarding the "So what should we do?" (which is an excellent way to end this issue!)
- Yes about capture, no about chunk. Or at least very uncertain about chunk. What we need to do is to figure out a way to teach Drasil about (at least) enumerated types, and probably about other kinds of 'semantic' types. What information we need to capture falls into two categories a. enough information to properly represent user's intent b. enough information to be able to generate code
- Strong no. These new types should be and large not be implemented with constraints unless that is the only way to do it in the target language. We should be trying to capture enough information to use each target language's type system (or equivalent) to do this.
