Added concrete par example from grammar. Added further elaboration on example. Other...
[firstyearreport:firstyearreport.git] / future.lhs
1
2 %include fhm-preamble.fmt
3 %include fhm-preamble-extras.fmt
4
5 \section{Future Work}
6 \label{sect:future}
7
8 Following on from the work described in Sect. \ref{sect:refined} there
9 are number of avenues for future research described in this section.
10
11 The goal of my thesis will be to develop and formalise a type theory
12 that captures, to a greater extent that previously possibly,
13 properties of modular systems of equations. These include properties
14 related to balance and structure, units-of-measure and structural
15 dynamism, among others. I intend to formalise the type system and
16 semantics of a pragmatic equation-based language in the
17 dependently-typed functional programming language Agda
18 \cite{Agdalang}.
19
20 \subsection{Compound Data Structures}
21 \label{sect:future:compound}
22
23 Compound data structures are an important aspect of almost every
24 modern programming language. Vectors and matrices are of particular
25 interest in modelling and form the basis for a huge number of
26 algorithms that emulate physical processes. 
27
28 Adding support for vectors to the \emph{functional} layer of our
29 system is a very well understood problem, and has been studied in
30 great depth \cite{Benton,Mottl,KuncakJackson,Hosoya}. However, adding
31 support for \emph{signal-level} vectors is a more challenging
32 problem. In particular, when combined with our structural type system,
33 detailed in Sect. \ref{sect:refined}, a number of questions
34 arise. Most notably, does a length $n$ vector of \emph{signal
35   variables} represent a single unknown, or $n$ unknowns?  Moreover,
36 what should be said about the contribution of an equation over such a
37 vector? Naturally, the above questions can be generalised from vectors
38 to arbitrary sized containers; for example, matrices, binary trees etc.
39
40 One approach might be to adapt the constraint approach outline in
41 Sect. \ref{sect:refined}. One could imagine assigning a fresh balance
42 variable to a vector that represents its size. Operations on a vector
43 would then generate constraints that refine the range of this
44 variables. Equations that mention a vector could then use said balance
45 variable to determine a contribution.
46
47 A more principled approach might be to index vectors with a natural
48 number representing length, a restricted form of dependent types
49 \cite{McKinna2006}. While this has obvious theoretical advantages, we
50 may lose a number of important properties of our type system, such as
51 type reconstruction and decidability. However, one could hope to find
52 a middle-ground that combines certain aspects of size indexing that
53 does not preclude desirable type system properties.
54
55 There are also a number of other pragmatic concerns related to balance
56 and structure checking that are yet to be considered. One such concern
57 is the integration of balance checking with explicit causality. A
58 user may mark certain unknowns as \emph{input} or \emph{output}
59 variables.  A \emph{real world} type checker would thus need to
60 consider the causality of variables when verifying structural
61 properties. Another concern is accommodating systems that are
62 \emph{intentionally unbalanced}. Redundant equations may sometimes be
63 required \cite{Nilsson2010} and conveying this information to the type
64 checker would be very useful.
65
66 \subsection{Type System Meta-Theory}
67 \label{sect:future:meta-theory}
68
69 In Sect. \ref{sect:refined} we developed a type system for a very
70 small equation-based language. It would be useful to verify the
71 meta-theoretic properties of the aforementioned system, primarily to
72 make it easier to predict the behaviour of the system, and also to
73 give us confidence that the theory and implementation are correct.
74 Specifically, we would like to show the soundness of the type system
75 with respect to our semantics.
76
77 The current type theory and semantics cover a small subset of the
78 functionality of FHM. It would be interesting to extend our calculus
79 to accommodate more advanced features. Doing so would demonstrate that
80 our type system interacts in a sound and predictable manner, and would
81 be instructive for integrating our refined types into similar
82 equation-based languages. This proposal is closely related to the
83 integration of compound data structures discussed in
84 Sect. \ref{sect:future:compound}.
85
86 \subsection{Structurally Dynamic System}
87 \label{sect:future:dynamic}
88
89 There is an obvious interaction between the FHM |switch| statements
90 (see Sect. \ref{sect:balance:meta:giorgidze}) and the type system
91 described in Sect. \ref{sect:refined}. Following Broman's notion of
92 type equality, one would only expect a system of equations to be
93 replaced by another if both systems contribute the same number of
94 equations. Hence, the following simple annotation of balance variables
95 could be used to enforce that all branches agree on their
96 contribution.
97 \begin{code}
98 switch :: SR (a , E b) n -> (b -> SR a n) -> SR a n
99 \end{code}
100
101 A more expressive, but equally more involved approach might be to
102 consider configuration switches in parallel. The idea of synchronised
103 switching has been suggested before \cite{Nikoukhah} and an example of
104 a practical application of such switches can be seen in Nilsson's
105 \cite{Nilsson2010} work on simulating ideal diodes. 
106
107 Suppose that two |switch| statements fire from the same event and
108 switch configurations at the same point in time. The weaker condition
109 that the two switches maintain the same \emph{net} contribution could
110 be enforced and would not require the two branches of a |switch|
111 statement to agree on their contribution, provided that the sum of all
112 parallel switches remained constant.
113
114 \subsection{Units-of-Measure}
115 \label{sect:future:units}
116
117 Sect. \ref{sect:balance:units} discusses the integration of
118 units-of-measure into programming languages. It would be interesting
119 to investigate the problems that arise when integrating such features
120 into FHM.
121
122 One such problem is the interaction between functional-level
123 dimensions and signal-level dimensions. Could the same system of
124 dimensions be used at both levels? If not, how would one marshal types
125 between the two levels?
126
127 Another consideration might be the expressivity of such a system of
128 dimensions. Even when one considers polymorphic recursion, there are
129 still terms that cannot be correctly inferred under Kennedy's inference
130 scheme. This suggests the need for some restricted form of dependent
131 types.