Merge branch 'master' of gitorious.org:tfp2010/tfp-paper
[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 \subsection{Adhering to Constraints}
363
364 There is little use in generating constraints without a mechanism to
365 check their consistency. To this end, the Fourier-Motzkin elimination
366 method is employed \cite{Kuhn}. The method allows one to
367 check not only if a set of linear inequalities is satisfiable, but
368 also finds a continuous interval for each bound variable. It is
369 expected that this will be useful when reporting type errors to the
370 programmer.
371
372 Constraint checking is necessary at two points during type checking.
373 Firstly, when a function application involves taking the union of two
374 sets of constraints, the newly constructed constraint set is checked
375 for consistency. Secondly, the types of let-bound expressions are
376 checked to ensure that all signal relations mentioned in a definition
377 are able to contribute a non-negative number of equations.
378
379 The elimination algorithm has worst case exponential time complexity
380 in the number of balance variables. However, as shown by Pugh
381 \cite{Pugh91}, the modified variant that searches for integer
382 solutions is capable of solving most common problem sets in low-order
383 polynomial time. Furthermore, systems typically involve only a handful
384 of balance variables, making it tractable to still check exponential
385 cases.
386
387 \subsection{Formalising the Type System}
388 \label{sec:type-sys-formalising} 
389
390 % * Brief recap of the strategy.
391 % * Explain syntax of types:
392 %   - SR p n
393 %   - Eqn n m o
394 %   - Pattern type (R,...,R)
395 %   - Constraint sets
396 %   - Quantification of balance and type variables.
397 % * Explain aspects of the typing rules
398 %   - Read-only environment I
399 %   - Bottom-up calculation of Eqn indices (m, n, o)
400 % * Brief overview of the typing algorithm?
401 % * Properties of the type system
402 %   - Totality, termination
403 %   - Totality, termination of Fourier-Motzkin
404 %   - Correctness w.r.t flattening semantics
405 % * Implementations of the ty pe system
406 %   - Haskell implementation
407 %   - Ongoing work toward Agda implementation
408
409 Fig. \ref{syntax:terms} from Sect. \ref{sec:type-sys-gs} provide the
410 syntax of terms and types upon which the typing judgements given in
411 Fig. \ref{fig:rules} are based.
412
413 The syntax of types is similar to that of the simply-typed
414 $\lambda$-calculus. The usual function type is augmented with 4
415 additional constructors for signal relations and equations.
416
417 Signal relation types mirror signal relation terms by recording the
418 cardinality of the set of variables, denoted |rm|. Additionally,
419 relations are annotated with a \emph{balance type variable} which may then
420 appear in a constraint set. Equation fragments may be assigned one of
421 the following types: |IEqn|, |LEqn|, or |MEqn|, representing equations
422 mentioning interface variables, local variables, and a mixture,
423 respectively. Type schemes are given by |sigma|, allowing types to be
424 constrained and polymorphic in the number of equations they
425 contribute. |C| and |ce| describe the syntax of constraints and
426 constraint expressions, respectively.
427
428 \begin{figure}[ht]
429 \centering 
430 \begin{mathpar}
431
432 \inferrule
433     {\Gamma (x) = C \Rightarrow \tau}
434     {\Gamma \vdash x : C \Rightarrow \tau}
435     \quad \textsc{(T--Var)}
436
437 \inferrule
438     {\Gamma,x:C_1 \Rightarrow \tau_1 \vdash e : C_2 \Rightarrow \tau_2}
439     {\Gamma \vdash \lambda x.e : C_1 \cup C_2 \Rightarrow \tau_1 \rightarrow \tau_2}
440     \quad \textsc{(T--Abs)}
441
442 \inferrule
443     {\Gamma \vdash e_1 : C_1 \Rightarrow \tau_2 \rightarrow \tau_1 
444      \and
445      \Gamma \vdash e_2 : C_2 \Rightarrow \tau_2}
446     {\Gamma \vdash e_1~e_2 : C_1 \cup C_2 \Rightarrow \tau_1}
447     \quad \textsc{(T--App)}
448
449 \inferrule
450     {\Gamma \vdash e_1 : C_1 \Rightarrow \tau_2
451      \and
452      \Gamma,x: C_2 \Rightarrow \tau_2 \vdash e_2 : C_1 \Rightarrow \tau_1 }
453     {\Gamma \vdash \textbf{let}~x=e_1~\textbf{in}~e_2 : C_1 \cup C_2 \Rightarrow \tau_1}
454     \quad \textsc{(T--Let)}
455
456 \inferrule
457     { }
458     {I\cdot\Gamma \vdash Atomic~\overline{z} : \emptyset \Rightarrow 
459       eqkind_I(\overline{z},1)}
460     \quad \textsc{(T--Atomic)}
461
462 \inferrule
463     {\Gamma \vdash e : C \Rightarrow |SR|~\rtothem~n
464      \and
465      \mathopen{||}\overline{z}\mathclose{||} \geq n
466     }
467     {I\cdot\Gamma \vdash e \diamond |(bar z)| : C \Rightarrow eqkind_I(|(bar z)|, n)}
468     \quad \textsc{(T--RelApp)}
469
470 \inferrule
471     {L=vars(\overline{q})\backslash \ \overline{z}
472      \and
473      %% \forall q \in \overline{q}.~\Gamma \vdash q : C_q \Rightarrow \tau_q
474      %% \overline{\Gamma \vdash {q} : c \Rightarrow \tau}^{~q \in \overline{q}}
475      \overline{z} \cdot \Gamma \vdash \overline{q} : \overline{C} \Rightarrow \overline{\tau}
476      \and
477      n_{X} = \Sigma \{~b~||~X\hspace{-0.3em}Eqn~b \in \overline{\tau}~\}
478      \\\\
479      C = \{ n = n_I + n_L + n_M - |abs L| , 0 \leq n \leq \mathopen{||}\overline{z}\mathclose{||} 
480             , n_I \leq  \mathopen{||}\overline{z}\mathclose{||}, n_L \leq |abs L| , n_L + n_M \geq |abs L| \}
481     }
482     {\Gamma \vdash \textbf{sigrel}~\overline{z}~\textbf{where}~\overline{q} 
483       : \bigcup \overline{C} \cup C \Rightarrow |SR|~ \mathbb{R}^{\mathopen{||}\overline{z}\mathclose{||}} ~n}
484
485 \end{mathpar}
486
487 \[
488 eqkind_I(Z,n) = 
489   \begin{cases}
490     IEqn~n & \text{if}~\emptyset \subset Z \subseteq I \\ 
491     LEqn~n & \text{if}~Z \cap I = \emptyset \\
492     MEqn~n & \text{otherwise}
493   \end{cases}
494 \]
495
496 \caption{Typing rules.}
497 \label{fig:rules}
498 \end{figure}
499
500 Fig. \ref{fig:rules} specifies 7 typing judgements for deriving types
501 in our type system. The rules for $\lambda$-terms are similar to those
502 of the simply-typed $\lambda$-calculus, with the addition of
503 constraint sets given by |C|. Operations that render a constraint
504 sets inconsistent indicate that a term is ill-typed.
505
506 \textsc{T-Atomic} and \textsc{T-RelApp} specify the rules for judging
507 the types of equations. These rules show how the integer indices of
508 the constructors of the form |XEqn| are calculated. These rules depend
509 on the read-only environment |I| which stores the set of interface
510 variables the equations range over. The remaining rule gives a
511 strategy for checking the types of signal relations, assigning a
512 balance, and generating constraints on that balance.
513
514 Balance type variables are treated in a similar manner to type
515 variables in the restricted polymorphic $\lambda$-calculus. Type
516 checking signal relations consists of generating a fresh balance type 
517 variable for the balance, and where necessary, constraining this
518 variable. Unifying two equations or signal relations proceeds as
519 expected by unifying the the appropriate balance variables.
520
521 The type system has been implemented in the functional programming
522 language Haskell. Furthermore, the totality and termination of the
523 algorithm have been mechanically verified using the dependently typed
524 programming language Agda \cite{Agda}. It should be noted that the
525 function for computing the \emph{most general unifier} of two types is
526 postulated, this is not a problem as it is well known that unification
527 is total and terminating \cite{DamasMilner}. The source code can be
528 found on the primary authors website at
529 \texttt{http://cs.nott.ac.uk/\textasciitilde jjc}.
530
531 \subsection{Small-step Semantics}
532
533 Fig. \ref{fig:semantics} presents the small-step semantics for our
534 calculus by way of a flattening for a system of equations. Values are
535 (sets of) atomic equations. The notation
536 $\{\overline{z_1}/\overline{z_2}\}$ denotes the substitution that
537 occurs when reducing signal relation application. Our abstract
538 treatment of equations allows us to read this notation as substituting
539 every variable in $\overline{z_1}$ for all variables in
540 $\overline{z_2}$, a simplification of the substitution given in
541 Sect. \ref{sec:mse-aosoe}.
542
543 \newcommand{\sigrel}[2]{\textbf{sigrel}~{#1}~\textbf{where}~{#2}}
544 \begin{figure}
545   \begin{mathpar}
546     \infer
547         {e_1 \leadsto e_2}
548         {e_1~e_3 \leadsto e_2~e_3}
549         \quad \textsc{(S-App1)}
550         
551     \infer
552         { }
553         {(\lambda x . e_1)~e_2 \leadsto [x \mapsto e_2]~e_1}
554         \quad \textsc{(S-App2)}
555
556     \infer
557         { }
558         {\textbf{let}~x = e_1~\textbf{in}~e_2 \leadsto [x \mapsto e_1]~e_2}
559         \quad \textsc{(S-Let)}
560
561     \infer
562         { }
563         {\sigrel{\emptyset}{v} \leadsto v}
564          \quad \textsc{(S-SigRel1)}
565
566     \infer
567      %% {\overline{q_1} \leadsto \overline{q_2}}
568         {\exists q_1 \in \overline{q}.~q_1 \leadsto q_2}
569         {\sigrel{\emptyset}{\overline{q}} \leadsto \sigrel{\emptyset}{[q_1 \mapsto q_2]~\overline{q}}}
570         \quad \textsc{(S-SigRel2)}
571
572     \infer
573         { }
574         {(\sigrel{\overline{z_1}}{\overline{q}}) \diamond \overline{z_2} \leadsto \{\overline{z_1}/\overline{z_2}\}~\overline{q}}
575         \quad \textsc{(S-SigApp1)}
576
577     \infer
578         {e_1 \leadsto e_2}
579         {e_1 \diamond \overline{z} \leadsto e_2 \diamond \overline{z}}
580         \quad \textsc{(S-SigApp2)}
581
582   \end{mathpar}
583   \caption{Small-step semantics.} 
584   \label{fig:semantics}
585 \end{figure}
586
587 The simplification of substitution discussed above has introduced a
588 slight disparity between our abstract formalisation and the concrete
589 system. In the FHM system, applying a signal relation contributing |n|
590 equations to a mixed set of variables results in |n| mixed
591 equations. However, during evaluation, it may be discovered that some
592 of the equations within the signal relation do not mention both local
593 and interface variables. Hence, the number of mixed, local, and
594 interface equations may be refined as a result of evaluation.
595
596 This problem is avoided in our semantics by the simplification to
597 substitution mentioned above. However, this should not pose a real
598 problem in the concrete system either. The preservation problem is
599 reminiscent of the record subtyping problem addressed in Peirce
600 \cite{Pierce}, pages 259--260. It should be possible to adapt the
601 technique of \emph{stupid casts} used in Pierce to solve the
602 preservation problems that would be present in a more concrete
603 semantics. To be more precise, one could allow a \emph{stupid cast} of
604 local and interface equations back into mixed equations, thus
605 retaining the same contribution and maintaining the same
606 constraints. We leave this alteration as future work, as the current
607 semantics are sufficient for the purposes of this paper.