Added concrete par example from grammar. Added further elaboration on example. Other...
[firstyearreport:firstyearreport.git] / refined.lhs
1
2 %include fhm-preamble.fmt
3 %include fhm-preamble-extras.fmt
4
5 \section{Type Checking Structural Properties}
6 \label{sect:refined}
7
8 In this section we discuss ongoing work by Capper and Nilsson
9 \cite{CapperNilsson} into capturing structural properties of modular,
10 first-class systems of equations using types.
11
12 The type system is presented as an embedding of an equation-based
13 language into the simply-typed $\lambda$-calculus. An embedding into
14 the $\lambda$-calculus reflects the two-level approach taken by FHM,
15 from which much of the expressivity of the language is gained. The
16 type system has been implemented in the dependently typed programming
17 language Agda \cite{Agdalang}, giving us assurances that the algorithm
18 is both total and terminating. Fig. \ref{fig:notation} gives the
19 notational conventions to be used throughout the remainder of this
20 section.
21
22 \newcommand\T{\rule{0pt}{2.6ex}}
23 \newcommand\B{\rule[-1.2ex]{0pt}{0pt}}
24
25 \begin{figure}[ht]
26 \centering
27 \begin{tabular}{ll}  
28   \hline
29   Description \T \B & Symbol \T \B \\
30   \hline \\
31   $\lambda$-bound variables     & |x, y| \\
32   Expressions ($\lambda$-terms) & |e| \\
33   Signal-variables              & |z| \\
34   Balance type-variables        & |n, m, o| \\
35   Equations                     & |q| \\
36   Simple types                  & |tau| \\
37   Constrained types             & |sigma| \\
38   Typing environments           & |Gamma| \\
39   Constraint sets               & |C| \\
40   Constraint expressions        & |c|
41 \end{tabular}
42 \caption{Notational Conventions}
43 \label{fig:notation}
44 \end{figure}
45
46 The notation $\overline{\chi}$ is used to denote a finite set. One
47 should also note that |x|, |y|, and |z| are \emph{meta-variables},
48 ranging over the names of concrete function-level and signal-level
49 variables, respectively.
50
51 To track the equation-variable balance, the type of a signal relation
52 is refined by annotating it with the number of equations it is able to
53 contribute to a system. The contribution of a signal relation may also
54 depend on the contribution of the parameters to the signal
55 relation. Hence, signal relations can behave in a polymorphic fashion,
56 contributing varying numbers of equations depending on the context in
57 which the relation is used. 
58  
59 Since the structural information required to determine a precise
60 contribution may not always be available, e.g. a model parameterised
61 by another model, the context in which a signal relation is applied is
62 used to generate \emph{balance constraints} (from now on, simply
63 constraints). These constraints restrict the balance of a component to
64 a contiguous interval.
65
66 Note that a representation of integers and linear inequalities has
67 been introduced at the type level. This extension may appear to be a
68 restricted form of dependent types \cite{McKinna2006}. However, these
69 type level representations, whilst determined by the structure of
70 terms, are not value level terms themselves. Therefore, we do not
71 consider our system to be dependently typed.
72
73 Constraints may involve the contributions of several components, and
74 hence are not directly associated with a single signal relation. As a
75 result, the type of a signal relation is restricted to being annotated
76 by a \emph{balance variable} which is then further refined using
77 constraints. The type checking algorithm generates a fresh balance
78 variable for each signal relation, with type equality defined up to
79 alpha equivalence of balance variables and the intervals of each
80 variable. To demonstrate, the refined type for |resistor| from
81 Sect.~\ref{sect:types-in-eq:hydra} is:
82 \begin{code}
83 resistor :: (n = 2) => Resistance -> SR (Pin, Pin) n
84 \end{code}
85 Haskell's type class constraint syntax has been adopted to express
86 that the balance type variable |n| is constrained to the value
87 |2|. This can be verified by first flattening the signal relation
88 applications to obtain a set of |3| equations over |5| variables (note
89 that each |Pin| contains two variables), then removing one equation
90 which must be used to solve for the local variable $u$, giving a net
91 contribution of two equations. An example involving multiple balance
92 variables can be found in Sect. \ref{sect:refined:constraints}.
93
94 In this paper, a signal relation will always have a determined size.
95 Afterall, a signal relation is just a collection of equations. Balance
96 variables are required when systems of equations are used as
97 parameters.
98
99 \subsection{Constraints}
100 \label{sect:refined:constraints}
101
102 It is conceivable that different application domains could generate
103 constraints specific to that domain. This is not a problem, as the
104 system developed is independent of the criteria used to generate
105 constraints, provided the constraints are linear inequalities.  For
106 the purposes of this report, 5 criteria for generating constraints
107 have been chosen. Before introducing the criteria, a number of
108 definitions are required.
109
110 Fig.~\ref{fig:syntax} gives the syntax of terms, types and constraints
111 of the $\lambda$-calculus augmented with a signal relation constructs.
112 These grammars emulate the two-level approach of FHM by embedding a
113 language of equations into a functional host language. Note that these
114 grammars represent a \emph{toy-language} that simulates the important
115 aspects of a two-level equation-based functional language, such as
116 FHM. The grammars do not attempt describe a comprehensive or
117 necessarily even a practical or useful modelling language.
118
119 \begin{figure}[h]
120 \begin{minipage}[t]{0.35\linewidth}
121 \begin{code}
122 e  ::=  x             
123    |    e1 e2
124    |    \x . e
125    |    let x = e1 in e2
126    |    sigrel (bar z) where (bar q)
127 ^^
128 q  ::=  atomic (bar z)
129    |    e <> (bar z)
130 \end{code}
131 \label{syntax:terms}
132 \end{minipage}
133 \begin{minipage}[t]{0.26\linewidth}
134 \begin{code}
135 sigma ::=  (bar C) => tau
136       |    (bar C) => rho
137 ^^
138 tau   ::=  tau1 -> tau2
139       |    SR n
140 ^^
141 rho   ::=  LEqn n
142       |    IEqn n
143       |    MEqn n
144 \end{code}
145 \label{syntax:types}
146 \end{minipage}
147 \begin{minipage}[t]{0.32\linewidth}
148 \begin{code}
149 C     ::=  c1 <= c2
150 ^^
151 c    ::=  n
152      |    INT
153      |    c + c
154      |    - c  
155 \end{code}
156 \label{syntax:constraints}
157 \end{minipage}
158 \vspace{-1.5em}
159 \caption{Syntax of terms, types, and constraints.}
160 \label{fig:syntax}
161 \end{figure}
162
163 The functional fragment is given by |e|, augmented with first-class
164 signal relation constructs. Signal relations abstract over sets
165 of signal variables, denoted $\overline{z}$, and embed a new syntactic
166 category of |equations| into the calculus, given by |q|.
167
168 Signal relations range over sets of equations, which may take one of
169 two forms. An atomic equation is an equation of the form |s1 = s2|,
170 where |s1| and |s2| are signal level expressions is abstracted to just
171 the set of distinct signal variables occurring in |s1| and
172 |s2|. Similarly, an equation of the form |e <> (bar s)| is abstracted
173 to the expression denoting the applied signal relation and the set of
174 signal variables that occur on the right-hand-side of the application.
175
176 An equation |q| is said to \emph{mention} a signal variable |z| if and
177 only if |z elem vars(q)|. The function |abs| takes a set of equations
178 and sums the \emph{contributions} of each equation.
179
180 \begin{minipage}{0.45\linewidth}
181 \begin{code}
182 vars (bar q) =
183   Union { vars' q | q elem (bar q) }
184   where
185     vars' (atomic (bar z))  = (bar z)
186     vars' (_ <> (bar z))    = (bar z)
187 \end{code}
188 \end{minipage}
189 \begin{minipage}{0.45\linewidth}
190 \begin{code}
191 abs (bar q) = Sum { size q | q elem (bar q) } 
192   where
193     size (atomic _)          = 1
194     size ((e : SR n) <>  _)  = n
195 \end{code}
196 \end{minipage}
197
198 %% \begin{minipage}{0.45\linewidth}
199 %% \begin{code}
200 %% vars (atomic (bar z))  = (bar z)
201 %% vars (_ <> (bar z))    = (bar z)
202 %% vars ((bar q))         = 
203 %%   Union { vars (q) | q elem (bar q) }
204 %% \end{code}
205 %% \end{minipage}
206 %% \begin{minipage}{0.45\linewidth}
207 %% \begin{code}
208 %% abs (atomic _)          = 1
209 %% abs (e : SR _ n <>  _)  = n
210 %% total ((bar q))           = 
211 %%   Sum { total (q) | q elem (bar q) } 
212 %% \end{code}
213 %% \end{minipage}
214
215 Given a signal relation |sigrel (bar z) where (bar q)|, the set of
216 interface variables is defined |subZ I = (bar z)|, and the set of
217 local variables | subZ L = (vars (bar q)) \\ (bar z) |. The set of
218 modular equations |(bar q)| can be partitioned into the disjoint
219 subsets of interface equations | subQ I |, local equations | subQ L |,
220 and mixed equations | subQ M |, where | subQ I | is the set of
221 equations mentioning only interface variables, | subQ L | is the set
222 of equations mentioning only local variables, and | subQ M = ((bar q)
223 \\ subQ I) \\ subQ L |. An equation that mentions no variables cannot
224 be used to solve for any unknowns, as such, we insist that valid
225 equations must mention at least one variable. The balance of a signal
226 relation is given by |bal = abs (bar q) - abs (subZ L)|.
227
228 %% Finally, the balance of a signal relation,
229 %% written |bal(sr)|, is given as |bal(sigrel (bar z) where (bar q)) =
230 %% total((bar q)) - abs(subQ L)|. Intuitively, balance is an aggregate of
231 %% the equations in the body of a signal relation, excluding sufficiently
232 %% many equations to solve for the local variables.
233
234 \begin{enumerate}
235
236 \item |abs(subQ L) + abs(subQ M) >= abs(subZ L)|. The local variables
237   are not under-constrained.
238
239 \item |abs(subQ L) <= abs(subZ L)|. The local variables are not
240   over-constrained.
241
242 \item |abs(subQ I) <= abs(subZ I)|. The interface variables are not
243   over-constrained.
244
245 \item |0 <= abs (bar q) + abs (subZ L)|. A signal relation should not
246   be capable of removing equations from other components (negative
247   contribution).
248
249 \item |abs (bar q) + abs (subZ L) <= abs (subZ I)|. A signal relation
250   can only contribute equations for variables present in its
251   interface.
252
253 %% \item |0 <= bal(sr) <= abs(subZ I)|. A signal relation must
254 %%   contribute equations only for its interface variables. It should not
255 %%   be capable of removing equations from other components (negative
256 %%   balance), or adding equations for variables not present in its
257 %%   interface.
258
259 \end{enumerate}
260
261 The above criteria produce constraints that give adequate assurances
262 for detecting structural anomalies. There is potential to further
263 refine these criteria, particularly for domain-specific
264 applications. However, for the purposes of this paper, these criteria
265 are sufficient to demonstrate the value of the type system.
266
267 To illustrate the application of the above four criteria, let us
268 revisit the |par| example from Sect. \ref{sect:types-in-eq:hydra}.
269 The underlying physics of this example is not important; the only
270 important aspect is that of equations \emph{mentioning} variables. The
271 type signature gives the type of |par| under the simply typed
272 approach. The reader may wish to refer back to
273 Sect. \ref{sect:types-in-eq:hydra} at this point for clarification on
274 |sigrel| constructs.
275
276 \noindent
277 \begin{minipage}{0.55\linewidth}
278 \begin{code}
279 par :: SR (Pin , Pin) -> SR (Pin ,  Pin)
280 par sr =
281     sigrel ((pi, pv), (ni, nv)) where
282       sr <> ((p1i, p1v), (n1i, n1v))
283       sr <> ((p2i, p2v), (n2i, n2v))
284       pi + p1i + p2i = 0
285       ni + n1i + n2i = 0
286       pv = p1v
287       pv = p2v
288       nv = n1v
289       nv = n2v
290 \end{code}
291 \end{minipage}
292 \begin{minipage}{0.45\linewidth}
293 \includegraphics{twoParRes.eps}
294 \vspace{0.9cm}
295 \end{minipage}
296
297 For instructive purposes, the above example is defined using FHM
298 syntax. There is obviously some tension between this definition and
299 the language defined by the grammar given in Fig. \ref{fig:syntax}.
300 Hence, the figure below shows how this example can be translated into
301 the simplified \emph{toy-language} used by the formalisation to
302 follow.
303
304 \noindent
305 \begin{code}
306 \sr -> sigrel {pi, pv, ni, nv} where {
307   sr <> {p1i, p1v, n1i, n1v},
308   sr <> {p2i, p2v, n2i, n2v},
309   atomic {pi, p1i, p2i},
310   atomic {ni, n1i, n2i},
311   atomic {pv, p1v},
312   atomic {pv, p2v},
313   atomic {nv, n1v, n2v} }
314 \end{code}
315
316 Under the new type system, the signal relation in |par| is annotated
317 by a balance variable which is then constrained by the criteria
318 producing the following refined type given below. Note that the
319 constraints are linear; scalar multiplication should be interpreted as
320 repeated addition. Additionally, a more flexible syntax for
321 constraints has been used for the sake of clarity: antisymmetry of
322 |<=| is exploited to achieve equality of constraints.
323 \[
324 par :: \left(
325   \begin{array}{c}
326     m = 2n - 2 \\
327     1 \leq n \leq 3 \\
328     0 \leq m \leq 4
329   \end{array}\right) \Rightarrow  
330     |SR|~(Pin , Pin)~n \rightarrow |SR|~(Pin , Pin)~m
331 \]
332
333
334
335 The constraints reflect the intuition of the |par| function. If a
336 resistor is connected in parallel with another resistor, then the
337 result is also resistor, i.e. one would expect the balance to be
338 preserved. Taking the balance of a resistor (|n|) to be |2|, as
339 calculated at the start of this section, we see that |par| does indeed
340 preserve this balance. The constraints on |par| show that |par| is
341 more flexible as it allows some flexibility in the balances of
342 component parameter.
343
344 It is also useful to see an example of a program that fails to type
345 check under the new type system -- a program that previously would
346 have been accepted, despite being faulty.
347
348 \begin{code}
349 broken sr = sigrel (a , b) where
350   sr <> (w + x , y + z)
351   sr <> (a , b)
352   x + z = 0
353 \end{code}
354
355 The above function |broken| is flawed in that there is no relation to
356 which it can be safely applied. The relation |sr| is required to
357 provide at least 3 equations for local variables $\{w,x,y,z\}$, but must not exceed
358 a contribution of 2 variables as dictated by the second relation
359 application. As expected, our type system catches this error by
360 attempting to impose the following inconsistent set of constraints:
361
362 \[
363 broken :: \left(
364   \begin{array}{c}
365     m = 2n - 3 \\
366     n = 3 \\
367     0 \leq m \leq 2 \\
368     0 \leq n \leq 2 \\
369   \end{array}\right) \Rightarrow  
370     |SR|~(\mathbb{R} , \mathbb{R})~n \rightarrow |SR|~(\mathbb{R} , \mathbb{R})~m
371 \]
372
373 It is possible to infer all balance variables and constraints without
374 requiring the programmer to annotate the terms explicitly.
375
376 During type checking, the Fourier-Motzkin elimination method
377 \cite{Kuhn} is used to check the consistency of constraint sets. The
378 method allows one to check not only if a set of linear inequalities is
379 satisfiable, but also finds a contiguous interval for each bound
380 variable. It is expected that this will be useful when reporting type
381 errors to the programmer.
382
383 The elimination algorithm has worst case exponential time complexity
384 in the number of balance variables. However, as shown by Pugh
385 \cite{Pugh91}, the modified variant that searches for integer
386 solutions is capable of solving most common problem sets in low-order
387 polynomial time. Furthermore, systems typically involve only a handful
388 of balance variables, making it feasible to check most exponential
389 cases.
390
391 \subsection{Formalising the Type System}
392 \label{sect:refined:formalising} 
393
394
395 Fig. \ref{fig:semantics} presents a small-step semantics for our
396 calculus by way of a flattening for a system of equations. Values in
397 our system are closed lambda-terms of the form |\x . e|, signal
398 relations encapsulating a flat set of equations, and atomic equations.
399
400 The notation $\{\overline{z_1}/\overline{z_2}\}$ denotes the
401 substitution that occurs when reducing signal relation
402 application. Our abstract treatment of equations allows us to read
403 this notation as substituting every variable in $\overline{z_1}$ for
404 all variables in $\overline{z_2}$, a simplification of the
405 substitution discussed in Sect. \ref{sect:types-in-eq:hydra}. The symbol
406 |fresh| denotes a fresh sequence of signal variables, used in
407 \textsc{S-SigApp2} to rename local variables to prevent name clashes
408 during flattening.
409
410 \newcommand{\sigrel}[2]{\textbf{sigrel}~{#1}~\textbf{where}~{#2}}
411 \begin{figure}
412   \begin{mathpar}
413     \infer
414         {e_1 \leadsto e_2}
415         {e_1~e_3 \leadsto e_2~e_3}
416         \quad \textsc{(S-App1)}
417         
418     \infer
419         { }
420         {(\lambda x . e_1)~e_2 \leadsto [x \mapsto e_2]~e_1}
421         \quad \textsc{(S-App2)}
422
423     \infer
424         { }
425         {\textbf{let}~x = e_1~\textbf{in}~e_2 \leadsto [x \mapsto e_1]~e_2}
426         \quad \textsc{(S-Let)}
427
428     \infer
429         {e_1 \leadsto e_2}
430         {e_1 \diamond \overline{z} \leadsto e_2 \diamond \overline{z}}
431         \quad \textsc{(S-SigApp1)}
432
433     \infer
434         {\exists q_1 \in \overline{q}.~q_1 \leadsto q_2}
435         {\sigrel{\overline{z}}{\overline{q}} \leadsto \sigrel{\overline{z}}
436           {[q_1 \mapsto q_2]~\overline{q}}}
437         \quad \textsc{(S-SigRel)}
438
439     \infer{\overline{q_2} = \{(vars(\overline{q})\backslash\overline{z_1})/
440             fresh\}~\overline{q_1} }
441         {(\sigrel{\overline{z_1}}{\overline{q_1}}) \diamond \overline{z_2} \leadsto 
442           \{\overline{z_1}/\overline{z_2}\}~\overline{q_2}}
443         \quad \textsc{(S-SigApp2)}
444
445   \end{mathpar}
446   \caption{Small-step semantics.} 
447   \label{fig:semantics}
448 \end{figure}
449
450 The simplification of substitution discussed above has introduced a
451 slight disparity between our abstract formalisation and the concrete
452 system. In the FHM system, applying a signal relation contributing |n|
453 equations to a mixed set of variables results in |n| mixed
454 equations. However, during evaluation, it may be discovered that some
455 of the equations within the signal relation do not mention both local
456 and interface variables. Hence, the number of mixed, local, and
457 interface equations may be refined as a result of evaluation.
458
459 This problem is avoided in our semantics by the simplification to
460 substitution mentioned above. However, this should not pose a real
461 problem in the concrete system either. The preservation problem is
462 reminiscent of the record subtyping problem addressed in Peirce
463 \cite{Pierce}, pages 259--260. It should be possible to adapt the
464 technique of \emph{stupid casts} used in Pierce to solve the 
465 preservation problems that would be present in a more concrete
466 semantics. To be more precise, one could allow a \emph{stupid cast} of
467 local and interface equations back into mixed equations, thus
468 retaining the same contribution and maintaining the same
469 constraints. We leave this alteration as future work, as the current
470 semantics are sufficient for the purposes of this report.
471
472 %% %% TYPING JUDGEMENTS
473
474 The syntax of types is similar to that of the simply-typed
475 $\lambda$-calculus. Simple types consist of functions, signal
476 relations, and equation types specified by |->|, |SR|, and
477 |I|/|M|/|LEqn| respectively. The three varieties of equation types
478 give distinct representations for interface, mixed, and local
479 equations. Signal relation types and equation types are parametrised
480 with a balance variable that denotes the number of equations a system
481 is capable of contributing. Simple types are then parametrised by a
482 constraint set that refines the possible interval of balance
483 variables.
484
485 \begin{figure}[ht]
486 \begin{minipage}[t]{0.40\linewidth}
487 \begin{code}
488 sub eqkind I (Z, n) = 
489     if emptyset subset Z subseteq I 
490         then IEqn n
491     else if Z intersect I = emptyset
492         then LEqn n
493         else MEqn n
494 \end{code}
495 \end{minipage}
496 \begin{minipage}[t]{0.50\linewidth}
497 \begin{code}
498 generate(n, sub n I, sub n L, sub n M, L, m) = {
499   n = sub n I + sub n L + sub n M - abs L, 
500   0 <= n ,
501   n <= m,
502   (sub n I) <= m ,
503   (sub n L) <= (abs L),
504   (abs L) <= sub n L + sub n M }
505 \end{code}
506 \end{minipage}
507 \caption{Auxiliary definitions}
508 \label{fig:aux-defs}
509 \end{figure}
510
511 Fig. \ref{fig:aux-defs} provides two auxiliary functions that are used
512 in the typing judgements. Given a set of signal variables the function
513 |eqkind| determines whether an equation is interface, local, or mixed
514 and returns the appropriate equation type. The function |generate|
515 constructs a constraint set for a signal relation.
516
517 \begin{figure}[ht]
518 \centering 
519 \begin{mathpar}
520
521 \inferrule
522     {\Gamma (x) = C \Rightarrow \tau}
523     {\Gamma \vdash x : C \Rightarrow \tau}
524     \quad \textsc{(T--Var)}
525
526 \inferrule
527     {\Gamma,x: \epsilon \Rightarrow \tau_1 \vdash e : C \Rightarrow \tau_2}
528     {\Gamma \vdash \lambda x.e : C \Rightarrow \tau_1 \rightarrow \tau_2}
529     \quad \textsc{(T--Abs)}
530
531 \inferrule
532     {C_1 \Rightarrow \tau_1 \equiv C_2 \Rightarrow \tau_2
533     \\\\
534     \Gamma \vdash e_1 : C_1 \Rightarrow \tau_1 \rightarrow \tau_3 
535      \and
536      \Gamma \vdash e_2 : C_2 \Rightarrow \tau_2}
537     {\Gamma \vdash e_1~e_2 : C_1 \cup C_2 \Rightarrow \tau_3}
538     \quad \textsc{(T--App)}
539
540 \inferrule
541     {\Gamma \vdash e_1 : C_1 \Rightarrow \tau_1
542      \and 
543      \Gamma,x : C_1 \Rightarrow \tau_1 \vdash e_2 : C_2 \Rightarrow \tau_2}
544     {\Gamma \vdash |let|~x = e_1~|in|~e_2 : C_2 \Rightarrow \tau_2}
545     \quad \textsc{(T--Let)}
546
547 \inferrule
548     { }
549     {I\cdot\Gamma \vdash \textbf{atomic}~\overline{z} : \epsilon \Rightarrow 
550       eqkind_I(\overline{z},1)}
551     \quad \textsc{(T--Atomic)}
552
553 \inferrule
554     {\Gamma \vdash e : C \Rightarrow |SR|~\rtothem~n
555      \and
556      \mathopen{||}\overline{z}\mathclose{||} \geq n
557     }
558     {I\cdot\Gamma \vdash e \diamond |(bar z)| : C \Rightarrow eqkind_I(|(bar z)|, n)}
559     \quad \textsc{(T--RelApp)}
560
561 \inferrule
562     {\overline{z} \cdot \Gamma \vdash \overline{q} : \overline{C} \Rightarrow \overline{\tau}
563      \and
564      n_{X} = \Sigma \{~b~||~X\hspace{-0.3em}Eqn~b \in \overline{\tau}~\}
565      \\\\
566      C = \bigcup \overline{C} \cup generate(n,~n_I,~n_L,~n_M,~
567        vars(\overline{q})\backslash \ \overline{z},~|abs (bar z)|)
568     }
569     {\Gamma \vdash \textbf{sigrel}~\overline{z}~\textbf{where}~\overline{q} 
570       : C \Rightarrow |SR|~ \mathbb{R}^{\mathopen{||}\overline{z}\mathclose{||}} ~n}
571     \quad \textsc{(T--SigRel)}
572
573 \end{mathpar}
574 \caption{Typing rules.}
575 \label{fig:rules}
576 \end{figure}
577
578 Fig. \ref{fig:rules} gives the typing rules for terms in our
579 language. The rules for $\lambda$-terms, \textsc{T-Var},
580 \textsc{T--Abs}, and \textsc{T--App} are similar to those of the
581 simply-typed $\lambda$-calculus, with the addition of constraint
582 sets. Operations that render a constraint sets inconsistent indicate
583 that a term is ill-typed; e.g, a judgement that involves taking the
584 union of two consistent sets of constraints is only valid when the
585 resulting constraint set is also consistent. The type equality $C_1
586 \Rightarrow \tau_1 \equiv C_2 \Rightarrow \tau_2 $ used in
587 \textsc{T--App} denotes that $\tau_1$ and $\tau_2$ are syntactically
588 equal up to a renaming of balance variables and that $C_1$ and $C_2$
589 constrain said balance variables to the same intervals.
590
591
592 The \textsc{T--Atomic} rule assigns equation types to atomic
593 equations by examining the variables that occur in the equation. The
594 helper function |eqkind| checks how the variables in an equation
595 coincide with the interface variables to determine whether the
596 equation is local, interface, or mixed.
597
598 The \textsc{T--RelApp} rule assigns an equation type to a relation
599 application. The preconditions for this judgement state that the type
600 of the expression |e| appearing to the left of the application must be
601 a signal relation. Additionally, the contribution of such a signal
602 relation must not exceed the number of interface variables to which it
603 is being applied. \textsc{T--RelApp} and \textsc{T--Atomic} depend on
604 the read-only environment |I| which stores the set of interface
605 variables the equations range over.
606
607 The \textsc{T--SigRel} rule assigns signal relation types to
608 |sigrel| constructs and calculates constraints on the fresh balance
609 variable of that signal relation. The first premise is a
610 point-wise judgement over the set of equations. The second premise
611 sums the number of equations of a given form in |bar q| specified by
612 the parameter |X|, where |X| $\in \{I,L,M\}$. Using the previous two
613 conditions, a set of constraints is generated for the balance
614 variables occurring in the type using the auxiliary |generate|
615 function.
616
617 We have identified two key properties of soundness for our type system
618 with respect to the semantics. Firstly, the preservation of types
619 under evaluation for |sigrel| constructs ensures that flattening a
620 modular system of equations does not alter the contribution of the
621 system. Formally, if |sigrel (bar z) where (bar q1)| $\leadsto$
622 |sigrel (bar z) where (bar q2)|, and |sigrel (bar z) where (bar
623 q1)|$~: C \Rightarrow$|SR|
624 $~\mathbb{R}^{\mathopen{||}\overline{z}\mathclose{||}}~n$, where |C|
625 is a consistent set of constraints, then |sigrel (bar z) where (bar
626 q2)|$ ~: C \Rightarrow$|SR|
627 $~\mathbb{R}^{\mathopen{||}\overline{z}\mathclose{||}}~n$. Hence, the
628 contribution of the sets of equations |q1| and |q2| is equal under the
629 same set of interface variables |(bar z)|.
630
631 Secondly, a system can only be completely reduced to a simple set of
632 equations if the top-level |sigrel| construct abstracts over an empty
633 set of signal variables.  In these circumstances, a fully assembled
634 system should contribute no equations as no more signal variables will
635 be introduced. Formally, if |sigrel emptyset| |where (bar q)|$~: C
636 \Rightarrow$|SR|$~()~n$, and |C| is consistent, then |C| should
637 resolve the interval of |n| to [0,0].
638
639 At this point, it is interesting to note the equational embedding
640 effectively operates as a form of heterogeneous meta-programming; a
641 modular system of equations is first evaluated to a flat set of
642 equations which is then transformed into a program that is used to
643 solve for the unknowns of the original system. Hence, the balance and
644 structure of a system of equations are really properties of the
645 flattened system of equations that rule out (a class of) \emph{second
646   stage} run-time/simulation-time problems. Hence, a soundness
647 statement regarding balance and structure falls to the meta-theory of
648 a type system at the second stage. In summary, attempting to capture
649 these properties during the initial phase make the soundness
650 properties of our system quite unusual. As such, we leave the
651 investigation of soundness of other structural properties as future
652 work.
653
654 The type checking algorithm has been implemented in the dependently
655 typed programming language Agda \cite{Agdalang}. The source code can
656 be found on the primary authors website at
657 \texttt{http://cs.nott.ac.uk/\textasciitilde jjc}. The implementation
658 guarantees that the algorithm is both total and terminating. It should
659 be noted that the function for computing the most general unifier of
660 two types is postulated. We have yet to implement the semantics and
661 prove that they are sound with respect to the typing judgements, this
662 is left as future work.
663
664 %% Space for more examples now?