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