Reordering of typing judgements and semantics.
[tfp2010:tfp-paper.git] / type-system.lhs
1
2 %include fhm-preamble.fmt
3 %include fhm-preamble-extras.fmt
4
5 \section{The Type System}
6 \label{sec:type-sys} 
7 % * Explain the basis of the type system
8 %   - Equational language embedded in the lambda-calculus
9 %   - Restricted system F.
10 %   - Hindley-Milner inference.
11 % - Notation conventions. 
12
13 The type system is presented as an embedding of an equation-based
14 language into the simply-typed $\lambda$-calculus. The type system has
15 been implemented in the dependently typed programming language Agda
16 \cite{Agda}, giving us assurances that the algorithm is both total
17 and terminating.
18
19 \newcommand\T{\rule{0pt}{2.6ex}}
20 \newcommand\B{\rule[-1.2ex]{0pt}{0pt}}
21
22 \begin{figure}
23 \begin{minipage}[b]{0.5\linewidth}
24 \centering
25 \begin{tabular}{ll}  
26   \hline
27   Description \T \B & Symbol \T \B \\
28   \hline \\
29   $\lambda$-bound variables     & |x|, |y| \\
30   Expressions ($\lambda$-terms) & |e| $\in\Lambda$ \\
31   Signal-variables              & |z| \\
32   Balance type-variables ~~~~~~ & |n|,|m|,|o| $\in\mathbb{Z}$ \\
33   Signal level expressions      & |s|
34 \end{tabular}
35 \end{minipage}
36 \begin{minipage}[b]{0.5\linewidth}
37 \centering
38 \begin{tabular}{ll} 
39  \hline
40   Description \T \B & Symbol \T \B \\ 
41   \hline \\
42   Equations                  & |q| \\
43   Simple types               & |tau| \\
44   Type schemes               & |sigma| \\
45   Typing environments ~~~~~~ & |Gamma| \\
46   Constraint sets            & |C|
47 \end{tabular}
48 \end{minipage}
49 \caption{Notation Conventions}
50 \label{fig:notation}
51 \end{figure}
52
53 The notation $\overline{\chi}$ is used to denote a sequence
54 $\chi_1,\ldots,\chi_n$ without repetition of elements. We will also
55 allow ourselves to treat $\overline{\chi}$ as sets equipped with the
56 usual set-theoretic operations. One should also note that |x| (and
57 |y|) and |z| are \emph{meta-variables}, ranging over the names of
58 concrete function-level and signal-level variables, respectively.
59
60 \subsection{Overview}
61
62 % * Motivation for using the type system
63 %   - We can only assume types are known.
64 %   - The structure of SR may also be unknown.
65 % * Outline of the refinements.
66 %   - SR types indexed by the number of equations they contribute.
67 %   - Both the structure and usage context of a signal relation
68 %     determine the balance constraints generated.
69 %   - Similar to dependent types, but far more restricted.
70 %   - Constraints may contain several balance variables, and as such
71 %     are separated from the ``types''. Adoption of Haskell style
72 %     class constraint syntax.
73
74 As signal relations are first-class entities, it cannot be assumed
75 that components can be flattened in order to determine the
76 equation-variable balance.
77 % The only reasonable assumption is that only
78 % the \emph{type} of a signal relation is known statically.
79 The only reasonable assumption is that all that is known statically
80 is the \emph{type} of a relation.
81
82 To track the equation-variable balance, the type of a signal relation
83 is refined by annotating it with the number of equations it is able to
84 contribute to a system. The contribution of a signal relation may also
85 depend on the contribution of the parameters to the signal
86 relation. Hence, signal relations can behave in a polymorphic fashion,
87 contributing varying numbers of equations depending on the context in
88 which the relation is used. See Sect. \ref{sec:related} for a
89 comparative review of alternative type system designs.
90
91 Since structural information required to determine a precise
92 contribution may not always be available, the context in which a
93 signal relation is applied is used to generate \emph{balance
94   constraints} (from now on, simply constraints). These constraints
95 restrict the balance of a component to an interval.
96
97 Note that a representation of integers and linear inequalities has
98 been introduced at the type level. This extension may appear to be a
99 restricted form of dependent types \cite{McKinna2006}. However, these
100 type level representations, whilst determined by the structure of
101 terms, are not value level terms themselves. As such, we do not
102 consider our system to be dependently typed.
103
104 Constraints may mention the contributions of several components, and
105 hence are not directly associated with a single signal relation. As a
106 result, the type of a signal relation is restricted to being annotated
107 by a \emph{balance variable} which is then further refined using
108 constraints. The type checking algorithm generates a fresh balance
109 variable for each signal relation, with type equality defined
110 up to alpha equivalence of balance variables. As an example, the
111 refined type for |resistor| from Sect.~\ref{sec:mse-fah} is:
112
113 > resistor :: (n = 2) => Resistance -> SR (Pin, Pin) n
114
115 Haskell's type class constraint syntax has been adopted to express
116 that the balance type variable |n| is constrained to the value
117 |2|. This can be verified by first flattening the signal relation
118 applications to obtain a set of |3| equations over |5| variables (note
119 that each |Pin| contains two variables), then removing one equation
120 which must be used to solve for the local variable $u$, giving a
121 contribution of two equations.
122
123 \subsection{Generating Constraints}
124 \label{sec:type-sys-gs}
125
126 % * Explain the purpose/requirement of the constraints
127 %   - What constraints to impose
128 %   - What impact these constraints have on type checking.
129 % * Define the simplified syntax of types and terms:
130 %   - Superficiality of simplifications
131 % * Formally define:
132 %   - Equations ``mentioning'' variables
133 %   - Number of concrete equations in a signal relation.
134 %   - Local and interface variables
135 %   - Local, interface and mixed equations
136 %   - Contribution of a signal relation.
137 % * Provide the 5 criteria.
138 % * Provide motivation example (par circuit)
139 %   - Show what constraints are generated for the example.  
140
141 Now let us consider constraint generation. It would be desirable to
142 catch as many faults in a system of equations as possible. However,
143 one cannot hope to retain a perfect interpretation of unsolvability of
144 variables in the type, instead an approximation must be admitted. This
145 is not a real issue as the goal of the proposed type system is not to
146 guarantee that a system of equations can be solved, but rather to
147 detect classes of errors that will definitely lead to structurally
148 unsound systems, e.g. unbalanced systems. 
149
150 This leads to the question of what constraints should be generated. It
151 is conceivable that different application domains could generate
152 constraints specific to that domain. This is not a problem, as the
153 system developed is independent of the constraints generated.  For the
154 purposes of this paper, 5 criteria for generating constraints have
155 been chosen. Before introducing the criteria, a number of definitions
156 are required.
157
158 Fig.~2 and 3 give the syntax of terms and types from which the type
159 checking algorithm will be developed. A number of simplifications have
160 been made to the FHM framework in order to keep the presentation of
161 the type system concise. Note that all simplifications are superficial
162 and do not fundamentally change the nature of the problem.
163 \begin{figure}
164 %% \vspace{-3em}
165 \begin{minipage}[t]{0.33\linewidth}
166 \centering
167 \begin{code}
168 e  ::=  x              
169    |    e1 e2
170    |    \x . e
171    |    let x = e1 in e2
172    |    sigrel (bar z) where (bar q)
173 ^^
174 q  ::=  Atomic (bar z)
175    |    e <> (bar z)
176 \end{code}
177 \label{syntax:terms}
178 \end{minipage}
179 \begin{minipage}[t]{0.33\linewidth}
180 \centering
181 \begin{code}
182 sigma ::=  overline C => tau
183 ^^
184 tau   ::=  tau1 -> tau2
185       |    SR rm n
186       |    LEqn n
187       |    IEqn n
188       |    MEqn n
189 \end{code}
190 \label{syntax:types}
191 \end{minipage}
192 \begin{minipage}[t]{0.32\linewidth}
193 \centering
194 \begin{code}
195 C     ::=  ce1 = ce2
196       |    ce1 >= ce2
197 ^^
198 ce    ::=  n
199       |    INT
200       |    ce + ce
201       |    - ce  
202 \end{code}
203 \label{syntax:constraints}
204 \end{minipage}
205 \vspace{-1.5em}
206 \caption{Syntax of terms, types, and constraints.}
207 \end{figure}
208
209 We consider the simply-typed $\lambda$-calculus, given by |e|,
210 augmented with first-class signal relation constructs. Signal
211 relations abstract over sets of signal variables, denoted $\overline{z}$,
212 and embed a new syntactic category of |equations| into the calculus,
213 given by |q|.
214
215 Signal relations range over sets of equations, which may take one of
216 two forms. An atomic equation of the form |s1 = s2| is abstracted to
217 just the set of distinct signal variables occurring in the signal
218 expressions |s1| and |s2|. Similarly, an equation of the form |e <>
219 (bar s)| is abstracted to the expression denoting the applied signal
220 relation and the set of signal variables that occur on the
221 right-hand-side of the application. More detailed comments on theses
222 syntactic categories are given in
223 Sect. \ref{sec:type-sys-formalising}.
224
225 An equation |q| is said to \emph{mention} a signal variable |z| if and
226 only if |z elem vars(q)|. The function |total| returns the raw number
227 of atomic equations contributed by an equation. On the other hand, |abs
228 (overline q)| denotes the cardinality of the set of \emph{modular}
229 equations.  Both |vars| and |total| are also overloaded for sets of
230 equations.
231
232 \begin{minipage}{0.45\linewidth}
233 \begin{code}
234 vars (Atomic (bar z))  = (bar z)
235 vars (_ <> (bar z))    = (bar z)
236 vars ((bar q))         = 
237   Union { vars (q) | q elem (bar q) }
238 \end{code}
239 \end{minipage}
240 \begin{minipage}{0.45\linewidth}
241 \begin{code}
242 total (Atomic _)          = 1
243 total (e : SR _ n <>  _)  = n
244 total ((bar q))           = 
245   Sum { total (q) | q elem (bar q) } 
246 \end{code}
247 \end{minipage}
248
249 Given a signal relation |sigrel (bar z) where (bar q)|, the set of
250 interface variables is defined |subZ I = (bar z)|, and the set of
251 local variables | subZ L = vars((bar q)) \\ (bar z) |. The set of
252 equations |(bar q)| can be partitioned into the disjoint subsets of
253 interface equations | subQ I |, local equations | subQ L |, and mixed
254 equations | subQ M |, where | subQ I | is the set of equations
255 mentioning only interface variables, | subQ L | is the set of
256 equations mentioning only local variables, and | subQ M = ((bar q)
257 \\ subQ I) \\ subQ L |. Finally, the balance of a signal relation is
258 written $bal(sr)$. It is now straightforward to specify the constraint
259 criteria:
260
261 %% Given a signal relation |sigrel (bar z) where (bar q)|, over a set of
262 %% signal variables |Z = (bar z) union vars((bar q))|, we define the set
263 %% of interface variables |subZ I = (bar z)|, and the set of local
264 %% variables | subZ L = vars((bar q)) \\ (bar z) |. The set of equations
265 %% |(bar q)| can be partitioned into the disjoint subsets of interface
266 %% equations | subQ I |, local equations | subQ L |, and mixed equations
267 %% | subQ M |, where | subQ I | is the set of equations mentioning only
268 %% interface variables, | subQ L | is the set of equations mentioning
269 %% only local variables, and | subQ M = ((bar q) \\ subQ I) \\ subQ L
270 %% |. Finally, the balance of a signal relation is written $bal(sr)$. It
271 %% is now straightforward to specify the constraint criteria:
272 \begin{enumerate}
273
274 \item |bal(sigrel (bar z) where (bar q)) = total((bar q)) - abs(subQ
275   L)|. The balance of a signal relation is an aggregate of the
276   equations in its body, excluding sufficiently many equations to solve for
277   the local variables.
278
279 \item |abs(subQ L) + abs(subQ M) >= abs(subZ L)|. The local variables
280   are not under-determined.
281
282 \item |abs(subQ L) <= abs(subZ L)|. The local variables are not
283   over-determined.
284
285 \item |abs(subQ I) <= abs(subZ I)|. The interface variables are not
286   over-determined.
287
288 \item |0 <= bal(sr) <= abs(subZ I)|. A signal relation must
289   contribute equations only for its interface variables. It should not
290   be capable of removing equations from other components (negative
291   balance), or adding equations for variables not present in its
292   interface.
293
294 \end{enumerate}
295
296 The above criteria produce constraints that give adequate assurances
297 for detecting structural anomalies. There is potential to further
298 refine these criteria. However, for the purposes of this paper, these
299 criteria are sufficient to demonstrate the value of the type system.
300
301 To illustrate the application of the above five criteria, consider the
302 Hydra example |par| that connects two circuit components in
303 parallel. The type signature gives the type of |par| under the simply
304 typed approach. The operational details of this example are not
305 important, the only important concept is that of equations
306 \emph{mentioning} variables.
307
308 \noindent
309 \begin{minipage}[b]{0.55\linewidth}
310 \begin{code}
311 par :: SR (Pin , Pin) -> SR (Pin ,  Pin) -> SR (Pin , Pin)
312 par sr1 sr2 =
313     sigrel ((pi, pv), (ni, nv)) where
314       sr1 <> ((p1i, p1v), (n1i, n1v))
315       sr2 <> ((p2i, p2v), (n2i, n2v))
316       pi + p1i + p2i = 0
317       ni + n1i + n2i = 0
318       pv = p1v = p2v
319       nv = n1v = n2v
320 \end{code}
321 \end{minipage}
322 \begin{minipage}[b]{0.45\linewidth}
323 \includegraphics{twoParRes.eps}
324 \vspace{0.9cm}
325 \end{minipage}
326
327 Under the new type system, the signal relations in |par| are annotated
328 by balance variables, which are then constrained by the criteria
329 producing the following refined type:
330
331 \begin{code}
332 par :: {  m = n + o - 2, 6 >= n + o >= 2, 0 <= m <= 4, 0 <= n <= 4, 0 <= o <= 4 } =>
333             SR (Pin , Pin) n -> SR (Pin , Pin) o -> SR (Pin , Pin) m
334 \end{code}
335
336 While this type may appear daunting at first, all balance variables
337 and constraints can be inferred without requiring the programmer to
338 annotate the terms explicitly.  It is also useful to see an example of
339 a program that fails to type check under the new type system -- a
340 program that previously would have been accepted, despite being
341 faulty.
342
343 \begin{code}
344 broken sr = sigrel (a , b) where
345   sr <> (w + x , y + z)
346   sr <> (a , b)
347   x + z = 0
348 \end{code}
349
350 The above function |broken| is flawed in that there is no relation to
351 which it can be safely applied. The relation |sr| is required to
352 provide at least 3 equations for local variables, but must not exceed
353 a contribution of 2 variables as dictated by the second relation
354 application. As expected, our type system catches this error by
355 attempting to impose the following inconsistent set of constraints:
356
357 \begin{code}
358 broken :: (m = n + n - 3, 0 <= m <= 2, 0 <= n <= 2, 4 <= n + 1 <= 4) 
359     => SR (Real , Real) n -> SR (Real , Real) m
360 \end{code}
361
362 There is little use in generating constraints without a mechanism to
363 check their consistency. To this end, the Fourier-Motzkin elimination
364 method is employed \cite{Kuhn}. The method allows one to
365 check not only if a set of linear inequalities is satisfiable, but
366 also finds a continuous interval for each bound variable. It is
367 expected that this will be useful when reporting type errors to the
368 programmer. 
369
370 The elimination algorithm has worst case exponential time complexity
371 in the number of balance variables. However, as shown by Pugh
372 \cite{Pugh91}, the modified variant that searches for integer
373 solutions is capable of solving most common problem sets in low-order
374 polynomial time. Furthermore, systems typically involve only a handful
375 of balance variables, making most exponential cases still feasible to
376 check.
377
378 \subsection{Formalising the Type System}
379 \label{sec:type-sys-formalising} 
380
381 % * Brief recap of the strategy.
382 % * Explain syntax of types:
383 %   - SR p n
384 %   - Eqn n m o
385 %   - Pattern type (R,...,R)
386 %   - Constraint sets
387 %   - Quantification of balance and type variables.
388 % * Explain aspects of the typing rules
389 %   - Read-only environment I
390 %   - Bottom-up calculation of Eqn indices (m, n, o)
391 % * Brief overview of the typing algorithm?
392 % * Properties of the type system
393 %   - Totality, termination
394 %   - Totality, termination of Fourier-Motzkin
395 %   - Correctness w.r.t flattening semantics
396 % * Implementations of the ty pe system
397 %   - Haskell implementation
398 %   - Ongoing work toward Agda implementation
399
400
401 Fig. \ref{syntax:terms} from Sect. \ref{sec:type-sys-gs} provide the
402 syntax of terms and types upon which the semantics and typing
403 judgements presented in this section are based.
404
405 Fig. \ref{fig:semantics} presents a small-step semantics for our
406 calculus by way of a flattening for a system of equations. Values in
407 our system are closed lambda-terms of the form |\x . e|, signal relations
408 encapsulating atomic equations, and atomic equations.
409
410 The notation $\{\overline{z_1}/\overline{z_2}\}$ denotes the
411 substitution that occurs when reducing signal relation
412 application. Our abstract treatment of equations allows us to read
413 this notation as substituting every variable in $\overline{z_1}$ for
414 all variables in $\overline{z_2}$, a simplification of the
415 substitution given in Sect. \ref{sec:mse-aosoe}. The symbol |fresh|
416 denotes a fresh sequence of signal variables, used in \textsc{S-SigApp2}
417 to rename local variables to prevent name clashes during flattening.
418
419 \newcommand{\sigrel}[2]{\textbf{sigrel}~{#1}~\textbf{where}~{#2}}
420 \begin{figure}
421   \begin{mathpar}
422     \infer
423         {e_1 \leadsto e_2}
424         {e_1~e_3 \leadsto e_2~e_3}
425         \quad \textsc{(S-App1)}
426         
427     \infer
428         { }
429         {(\lambda x . e_1)~e_2 \leadsto [x \mapsto e_2]~e_1}
430         \quad \textsc{(S-App2)}
431
432     \infer
433         { }
434         {\textbf{let}~x = e_1~\textbf{in}~e_2 \leadsto [x \mapsto e_1]~e_2}
435         \quad \textsc{(S-Let)}
436
437     \infer
438         {e_1 \leadsto e_2}
439         {e_1 \diamond \overline{z} \leadsto e_2 \diamond \overline{z}}
440         \quad \textsc{(S-SigApp1)}
441
442     \infer
443         {\exists q_1 \in \overline{q}.~q_1 \leadsto q_2}
444         {\sigrel{\overline{z}}{\overline{q}} \leadsto \sigrel{\overline{z}}
445           {[q_1 \mapsto q_2]~\overline{q}}}
446         \quad \textsc{(S-SigRel)}
447
448     \infer{\overline{q_2} = \{(vars(\overline{q})\backslash\overline{z_1})/
449             fresh\}~\overline{q_1} }
450         {(\sigrel{\overline{z_1}}{\overline{q_1}}) \diamond \overline{z_2} \leadsto 
451           \{\overline{z_1}/\overline{z_2}\}~\overline{q_2}}
452         \quad \textsc{(S-SigApp2)}
453
454   \end{mathpar}
455   \caption{Small-step semantics.} 
456   \label{fig:semantics}
457 \end{figure}
458
459 The simplification of substitution discussed above has introduced a
460 slight disparity between our abstract formalisation and the concrete
461 system. In the FHM system, applying a signal relation contributing |n|
462 equations to a mixed set of variables results in |n| mixed
463 equations. However, during evaluation, it may be discovered that some
464 of the equations within the signal relation do not mention both local
465 and interface variables. Hence, the number of mixed, local, and
466 interface equations may be refined as a result of evaluation.
467
468 This problem is avoided in our semantics by the simplification to
469 substitution mentioned above. However, this should not pose a real
470 problem in the concrete system either. The preservation problem is
471 reminiscent of the record subtyping problem addressed in Peirce
472 \cite{Pierce}, pages 259--260. It should be possible to adapt the
473 technique of \emph{stupid casts} used in Pierce to solve the
474 preservation problems that would be present in a more concrete
475 semantics. To be more precise, one could allow a \emph{stupid cast} of
476 local and interface equations back into mixed equations, thus
477 retaining the same contribution and maintaining the same
478 constraints. We leave this alteration as future work, as the current
479 semantics are sufficient for the purposes of this paper.
480
481 The syntax of types is similar to that of the simply-typed
482 $\lambda$-calculus. The usual function type is augmented with 4
483 additional constructors for signal relations and equations.
484
485 Signal relation types mirror signal relation terms by recording the
486 cardinality of the set of variables, denoted |rm|. Additionally,
487 relations are annotated with a \emph{balance type variable} which may then
488 appear in a constraint set. Equation fragments may be assigned one of
489 the following types: |IEqn|, |LEqn|, or |MEqn|, representing equations
490 mentioning interface variables, local variables, and a mixture,
491 respectively. Type schemes are given by |sigma|, allowing types to be
492 constrained and polymorphic in the number of equations they
493 contribute. |C| and |ce| describe the syntax of constraints and
494 constraint expressions, respectively.
495
496 \begin{figure}[ht]
497 \centering 
498 \begin{mathpar}
499
500 \inferrule
501     {\Gamma (x) = C \Rightarrow \tau}
502     {\Gamma \vdash x : C \Rightarrow \tau}
503     \quad \textsc{(T--Var)}
504
505 \inferrule
506     {\Gamma,x:C_1 \Rightarrow \tau_1 \vdash e : C_2 \Rightarrow \tau_2}
507     {\Gamma \vdash \lambda x.e : C_1 \cup C_2 \Rightarrow \tau_1 \rightarrow \tau_2}
508     \quad \textsc{(T--Abs)}
509
510 \inferrule
511     {\Gamma \vdash e_1 : C_1 \Rightarrow \tau_2 \rightarrow \tau_1 
512      \and
513      \Gamma \vdash e_2 : C_2 \Rightarrow \tau_2}
514     {\Gamma \vdash e_1~e_2 : C_1 \cup C_2 \Rightarrow \tau_1}
515     \quad \textsc{(T--App)}
516
517 \inferrule
518     {\Gamma \vdash e_1 : C_1 \Rightarrow \tau_2
519      \and
520      \Gamma,x: C_2 \Rightarrow \tau_2 \vdash e_2 : C_1 \Rightarrow \tau_1 }
521     {\Gamma \vdash \textbf{let}~x=e_1~\textbf{in}~e_2 : C_1 \cup C_2 \Rightarrow \tau_1}
522     \quad \textsc{(T--Let)}
523
524 \inferrule
525     { }
526     {I\cdot\Gamma \vdash Atomic~\overline{z} : \emptyset \Rightarrow 
527       eqkind_I(\overline{z},1)}
528     \quad \textsc{(T--Atomic)}
529
530 \inferrule
531     {\Gamma \vdash e : C \Rightarrow |SR|~\rtothem~n
532      \and
533      \mathopen{||}\overline{z}\mathclose{||} \geq n
534     }
535     {I\cdot\Gamma \vdash e \diamond |(bar z)| : C \Rightarrow eqkind_I(|(bar z)|, n)}
536     \quad \textsc{(T--RelApp)}
537
538 \inferrule
539     {L=vars(\overline{q})\backslash \ \overline{z}
540      \and
541      %% \forall q \in \overline{q}.~\Gamma \vdash q : C_q \Rightarrow \tau_q
542      %% \overline{\Gamma \vdash {q} : c \Rightarrow \tau}^{~q \in \overline{q}}
543      \overline{z} \cdot \Gamma \vdash \overline{q} : \overline{C} \Rightarrow \overline{\tau}
544      \and
545      n_{X} = \Sigma \{~b~||~X\hspace{-0.3em}Eqn~b \in \overline{\tau}~\}
546      \\\\
547      C = \{ n = n_I + n_L + n_M - |abs L| , 0 \leq n \leq \mathopen{||}\overline{z}\mathclose{||} 
548             , n_I \leq  \mathopen{||}\overline{z}\mathclose{||}, n_L \leq |abs L| , n_L + n_M \geq |abs L| \}
549     }
550     {\Gamma \vdash \textbf{sigrel}~\overline{z}~\textbf{where}~\overline{q} 
551       : \bigcup \overline{C} \cup C \Rightarrow |SR|~ \mathbb{R}^{\mathopen{||}\overline{z}\mathclose{||}} ~n}
552
553 \end{mathpar}
554
555 \[
556 eqkind_I(Z,n) = 
557   \begin{cases}
558     IEqn~n & \text{if}~\emptyset \subset Z \subseteq I \\ 
559     LEqn~n & \text{if}~Z \cap I = \emptyset \\
560     MEqn~n & \text{otherwise}
561   \end{cases}
562 \]
563
564 \caption{Typing rules.}
565 \label{fig:rules}
566 \end{figure}
567
568 Fig. \ref{fig:rules} specifies 7 typing judgements for deriving types
569 in our type system. The rules for $\lambda$-terms are similar to those
570 of the simply-typed $\lambda$-calculus, with the addition of
571 constraint sets given by |C|. Operations that render a constraint
572 sets inconsistent indicate that a term is ill-typed.
573
574 \textsc{T-Atomic} and \textsc{T-RelApp} specify the rules for judging
575 the types of equations. These rules show how the integer indices of
576 the constructors of the form |XEqn| are calculated. These rules depend
577 on the read-only environment |I| which stores the set of interface
578 variables the equations range over. The remaining rule gives a
579 strategy for checking the types of signal relations, assigning a
580 balance, and generating constraints on that balance.
581
582 Balance type variables are treated in a similar manner to type
583 variables in the restricted polymorphic $\lambda$-calculus. Type
584 checking signal relations consists of generating a fresh balance type 
585 variable for the balance, and where necessary, constraining this
586 variable. Unifying two equations or signal relations proceeds as
587 expected by unifying the the appropriate balance variables.
588
589 The type system has been implemented in the functional programming
590 language Haskell. Furthermore, the totality and termination of the
591 algorithm have been mechanically verified using the dependently typed
592 programming language Agda \cite{Agda}. It should be noted that the
593 function for computing the \emph{most general unifier} of two types is
594 postulated, this is not a problem as it is well known that unification
595 is total and terminating \cite{DamasMilner}. The source code can be
596 found on the primary authors website at
597 \texttt{http://cs.nott.ac.uk/\textasciitilde jjc}.
598