You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: spec/typing.md
+23-11Lines changed: 23 additions & 11 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -12,25 +12,25 @@ We define the GraphAlg type system formally using [typing rules](https://en.wiki
12
12
13
13
### Environments
14
14
Typing rules use three distinct environments:
15
-
- Function environment $F$: Associates function names with the parameter and results types of those functions.
15
+
- Function environment $$F$$: Associates function names with the parameter and results types of those functions.
16
16
- Dimension environment $D$: Associates variable names with dimension symbols.
17
17
- Local environment $L$: Associates variable names with a matrix type.
18
18
19
19
The environment objects have map semantics:
20
20
- $M \in L$ asserts that $L$ contains a value for $M$.
21
-
- $L[M]$ retrieves the value for key $M$ from environment $L$.
21
+
- $L[M]$ retrieves the value for key $M$ from environment $L$.
22
22
Implies $M \in L$.
23
-
- $L' := L[M := \tau]$ creates an updated environment $L'$ that contains all mappings from $L$ plus a mapping from $M$ to $\tau$.
23
+
- $L' := L[M := \tau]$ creates an updated environment $L'$ that contains all mappings from $L$ plus a mapping from $M$ to $\tau$.
24
24
If $M \in L$, then the original value for $M$ is dropped ($L'[M] = \tau$).
25
25
26
26
### Type Instances
27
-
Type instances are denoted $\langle d_1, d_2, R \rangle$, where
28
-
- $d_1$ is the dimension symbol for the number of rows
27
+
Type instances are denoted $\langle d_1, d_2, R \rangle$, where
28
+
- $d_1$ is the dimension symbol for the number of rows
29
29
- $d_2$ is the dimension symbol for the number of columns
30
30
- $R$ is the semiring
31
31
32
32
### Bindings
33
-
We use the syntax $A := B$ to bind the value of $B$ to a new variable $A$.
33
+
We use the syntax $A := B$ to bind the value of $B$ to a new variable $A$.
34
34
This binding syntax is also used to destructure types, e.g. $\langle d_1, d_2, R \rangle := \tau$ allows referencing the dimension symbols and the semiring of $\tau$. Furthermore, the syntax can also be used for asserting (partial) matches. For example, the statement $\langle d, 1, R_1 \rangle = \tau_1$ following by $\langle 1, d, R_2 \rangle$ asserts that:
35
35
- $\tau_1$ has one column
36
36
- $\tau_2$ has one row
@@ -40,8 +40,8 @@ No requirement is placed on the relation of $R_1$ and $R_2$: they may refer to t
40
40
41
41
## Functions
42
42
Functions have a function type of the form $(\tau_1 \times \tau_2) \rightarrow \tau_r$.
43
-
A program is nothing more than a collection of functions.
44
-
Note that the order in which functions are defined is significant:
43
+
A program is nothing more than a collection of functions.
44
+
Note that the order in which functions are defined is significant:
45
45
A function cannot be referenced before they are defined.
46
46
47
47
<imgsrc="latex/program.svg"width="600"/>
@@ -53,7 +53,7 @@ Statements update the $D$ and $L$ environments.
53
53
They do not have a type of their own.
54
54
55
55
### Assign
56
-
If there is no existing binding for the variable to be assigned, the first rule applies.
56
+
If there is no existing binding for the variable to be assigned, the first rule applies.
57
57
Otherwise, the more involved reassignment rule applies.
58
58
59
59
<imgsrc="latex/stmt-assign.svg"width="600"/>
@@ -107,7 +107,7 @@ Transpose is valid for any input matrix.
107
107
<imgsrc="latex/expr-diag.svg"width="600"/>
108
108
109
109
### `apply`
110
-
Functions used in `apply` must be defined over scalar input and output types.
110
+
Functions used in `apply` must be defined over scalar input and output types.
111
111
The parameter semirings must match those of the respective input arguments.
112
112
113
113
<imgsrc="latex/expr-apply.svg"width="600"/>
@@ -149,7 +149,7 @@ Operations such as subtraction or division are only allowed on specific semiring
149
149
<imgsrc="latex/expr-arith.svg"width="600"/>
150
150
151
151
### Scalar Compare
152
-
Ordered comparison operations are only allowed on the `int` and `real` semirings.
152
+
Ordered comparison operations are only allowed on the `int` and `real` semirings.
153
153
Equality comparison is allowed regardless of the semiring.
154
154
155
155
<imgsrc="latex/expr-compare.svg"width="600"/>
@@ -158,3 +158,15 @@ Equality comparison is allowed regardless of the semiring.
158
158
Literals must be valid for the specified semiring.
0 commit comments