\chapter[chap:future]{Future work}
\section{Improved notation for hierarchical state}
-The hierarchic state model requires quite some boilerplate code for unpacking
+The hierarchical state model requires quite some boilerplate code for unpacking
and distributing the input state and collecting and repacking the output
-state. There is really only one way in which this state handling can be done,
-so it would make sense to hide this boilerplate. This would incur no
-flexibility cost at all, since there are no other ways that would work.
+state.
-Options: Misuse the do notation in Haskell, create some abstraction in
-Haskell or add new syntax.
+\in{Example}[ex:NestedState] shows a simple composition of two stateful
+functions, \hs{funca} and \hs{funcb}. The state annotation using the
+\hs{State} newtype has been left out, for clarity and because the proposed
+approach below cannot handle that (yet).
-\section{Improved notation or abstraction for pipelining}
+\startbuffer[NestedState]
+ type FooState = ( AState, BState )
+ foo :: Word -> FooState -> (FooState, Word)
+ foo in s = (s', outb)
+ where
+ (sa, sb) = s
+ (sa', outa) = funca in sa
+ (sb', outb) = funcb outa sb
+ s' = (sa', sb')
+\stopbuffer
+\placeexample[here][ex:NestedState]{Simple function composing two stateful
+ functions.}{\typebufferhs{NestedState}}
+
+Since state handling always follows strict rules, there is really no other way
+in which this state handling can be done (you can of course move some things
+around from the where clause to the pattern or vice versa, but it would still
+be effectively the same thing). This means it makes extra sense to hide this
+boilerplate away. This would incur no flexibility cost at all, since there are
+no other ways that would work.
+
+One particular notation in Haskell that seems promising, is the \hs{do}
+notation. This is meant to simplify Monad notation by hiding away some
+details. It allows one to write a list of expressions, which are composited
+using the monadic \emph{bind} operator, written in Haskell as \hs{>>}. For
+example, the snippet:
+
+\starthaskell
+do
+ somefunc a
+ otherfunc b
+\stophaskell
+
+will be desugared into:
+
+\starthaskell
+(somefunc a) >> (otherfunc b)
+\stophaskell
+
+\todo{Properly introduce >>=}
+There is also the \hs{>>=} operator, which allows for passing variables from
+one expression to the next. If we could use this notation to compose a
+stateful computation from a number of other stateful functions, this could
+move all the boilerplate code into the \hs{>>} operator. Perhaps the compiler
+should be taught to always inline the \hs{>>} operator, but after that there
+should be no further changes required to the compiler.
+
+This is highlights an important aspect of using a functional language for our
+descriptions: We can use the language itself to provide abstractions of common
+patterns, making our code smaller.
+
+\subsection{Breaking out of the Monad}
+However, simply using the monad notation is not as easy as it sounds. The main
+problem is that the Monad type class poses a number of limitations on the
+bind operator \hs{>>}. Most importantly, it has the following type signature:
+
+\starthaskell
+(>>) :: (Monad m) => m a -> m b -> m b
+\stophaskell
+
+This means that any expression in our composition must use the same Monad
+instance as its type, only the "return" value can be different between
+expressions.
+
+Ideally, we would like the \hs{>>} operator to have a type like the following
+\starthaskell
+type Stateful s r = s -> (s, r)
+(>>) :: Stateful s1 r1 -> Stateful s2 r2 -> Stateful (s1, s2) r2
+\stophaskell
+
+What we see here, is that when we compose two stateful functions (whose inputs
+have already been applied, leaving just the state argument to be applied), the
+result is again a stateful function whose state is composed of the two
+\emph{substates}. The return value is simply the return value of the second
+function, discarding the first (to preserve that one, the \hs{>>=} operator
+can be used).
+
+There is a trick we can apply to change the signature of the \hs{>>} operator.
+\small{GHC} does not require the bind operators to be part of the \hs{Monad}
+type class, as long as it can use them to translate the do notation. This
+means we can define our own \hs{>>} and \hs{>>=} operators, outside of the
+\hs{Monad} typeclass. This does conflict with the existing methods of the
+\hs{Monad} typeclass, so we should prevent \small{GHC} from loading those (and
+all of the Prelude) by passing \type{-XNoImplicitPrelude} to \type{ghc}. This
+is slightly inconvenient, but since we hardly using anything from the prelude,
+this is not a big problem. We might even be able to replace some of the
+Prelude with hardware-translateable versions by doing this.
+
+We can now define the following binding operators. For completeness, we also
+supply the return function, which is not called by \small{GHC} implicitely,
+but can be called explicitely by a hardware description.
+
+\starthaskell
+(>>) :: Stateful s1 r1 -> Stateful s2 r2 -> Stateful (s1, s2) r2
+f1 >> f2 = f1 >>= \_ -> f2
+
+(>>=) :: Stateful s1 r1 -> (r1 -> Stateful s2 r2) -> Stateful (s1, s2) r2
+f1 >>= f2 = \(s1, s2) -> let (s1', r1) = f1 s1
+ (s2', r2) = f2 r1 s2
+ in ((s1', s2'), r2)
+
+return :: r -> Stateful () r
+return r = \s -> (s, r)
+\stophaskell
+
+As you can see, this closely resembles the boilerplate of unpacking state,
+passing it to two functions and repacking the new state. With these
+definitions, we could have writting \in{example}[ex:NestedState] a lot
+shorter, see \in{example}[ex:DoState]. In this example the type signature of
+foo is the same (though it is now written using the \hs{Stateful} type
+synonym, it is still completely equivalent to the original: \hs{foo :: Word ->
+FooState -> (FooState, Word)}.
+
+Note that the \hs{FooState} type has changed (so indirectly the type of
+\hs{foo} as well). Since the state composition by the \hs{>>} works on two
+stateful functions at a time, the final state consists of nested two-tuples.
+The final \hs{()} in the state originates from the fact that the \hs{return}
+function has no real state, but is part of the composition. We could have left
+out the return statement (and the \hs{outb <-} part) to make \hs{foo}'s return
+value equal to \hs{funcb}'s, but this approach makes it clearer what is
+happening.
+
+\startbuffer[DoState]
+ type FooState = ( AState, (BState, ()) )
+ foo :: Word -> Stateful FooState Word
+ foo in = do
+ outa <- funca in
+ outb <- funcb outa
+ return outb
+\stopbuffer
+\placeexample[here][ex:DoState]{Simple function composing two stateful
+ functions, using do notation.}
+ {\typebufferhs{DoState}}
+
+An important implication of this approach is that the order of writing
+function applications affects the state type. Fortunately, this problem can be
+localized by consistently using type synonyms for state types, which should
+prevent changes in other function's source when a function changes.
+
+A less obvous implications of this approach is that the scope of variables
+produced by each of these expressions (using the \hs{<-} syntax) is limited to
+the expressions that come after it. This prevents values from flowing between
+two functions (components) in two directions. For most Monad instances, this
+is a requirement, but here it could have been different.
+
+\todo{Add examples or reference for state synonyms}
+
+\subsection{Alternative syntax}
+Because of these typing issues, misusing Haskell's do notation is probably not
+the best solution here. However, it does show that using fairly simple
+abstractions, we could hide a lot of the boilerplate code. Extending
+\small{GHC} with some new syntax sugar similar to the do notation might be a
+feasible.
+
+\section[sec:future:pipelining]{Improved notation or abstraction for pipelining}
Since pipelining is a very common optimization for hardware systems, it should
-be easy to specify a pipelined system. Since it involves quite some registers
+be easy to specify a pipelined system. Since it introduces quite some registers
into an otherwise regular combinatoric system, we might look for some way to
abstract away some of the boilerplate for pipelining.
-Example of naive pipelined code
+Something similar to the state boilerplate removal above might be appropriate:
+Abstract away some of the boilerplate code using combinators, then hide away
+the combinators in special syntax. The combinators will be slightly different,
+since there is a (typing) distinction between a pipeline stage and a pipeline
+consisting of multiple stages. Also, it seems necessary to treat either the
+first or the last pipeline stage differently, to prevent an off-by-one error
+in the amount of registers (which is similar to the extra \hs{()} state type
+in \in{example}[ex:DoState], which is harmless there, but would be a problem
+if it introduced an extra, useless, pipeline stage).
+
+This problem is slightly more complex than the problem we've seen before. One
+significant difference is that each variable that crosses a stage boundary
+needs a register. However, when a variable crosses multiple stage boundaries,
+it must be stored for a longer period and should receive multiple registers.
+Since we can't find out from the combinator code where the result of the
+combined values is used (at least not without using Template Haskell to
+inspect the \small{AST}), there seems to be no easy way to find how much
+registers are needed.
+
+There seem to be two obvious ways of handling this problem:
+
+\startitemize
+ \item Limit the scoping of each variable produced by a stage to the next
+ stage only. This means that any variables that are to be used in subsequent
+ stages should be passed on explicitely, which should allocate the required
+ number of registers.
+
+ This produces cumbersome code, where there is still a lot of explicitness
+ (though this could be hidden in syntax sugar).
+ \todo{The next sentence is unclear}
+ \item Scope each variable over every subsequent pipeline stage and allocate
+ the maximum amount of registers that \emph{could} be needed. This means we
+ will allocate registers that are never used, but those could be optimized
+ away later. This does mean we need some way to introduce a variable number
+ of variables (depending on the total number of stages), assign the output of
+ a different register to each (\eg., a different part of the state) and scope
+ a different one of them over each the subsequent stages.
+
+ This also means that when adding a stage to an existing pipeline will change
+ the state type of each of the subsequent pipeline stages, and the state type
+ ofthe added stage depends on the number of subsequent stages.
+
+ Properly describing this will probably also require quite explicit syntax,
+ meaning this is not feasible without some special syntax.
+\stopitemize
+
+Some other interesting issues include pipeline stages which are already
+stateful, mixing pipelined with normal computation, etc.
+
+\section{Recursion}
+The main problems of recursion have been described in
+\in{section}[sec:recursion]. In the current implementation, recursion is
+therefore not possible, instead we rely on a number of implicitly list-recursive
+builtin functions.
+
+Since recursion is a very important and central concept in functional
+programming, it would very much improve the flexibility and elegance of our
+hardware descriptions if we could support (full) recursion.
+
+For this, there are two main problems to solve:
+
+\startitemize
+\item For list recursion, how to make a description type check? It is quite
+possible that improvements in the \small{GHC} typechecker will make this
+possible, though it will still stay a challenge. Further advances in
+dependent typing support for Haskell will probably help here as well.
+
+\todo{Reference Christiaan and other type-level work
+(http://personal.cis.strath.ac.uk/conor/pub/she/)}
+\item For all recursion, there is the obvious challenge of deciding when
+recursion is finished. For list recursion, this might be easier (Since the
+base case of the recursion influences the type signatures). For general
+recursion, this requires a complete set of simplification and evaluation
+transformations to prevent infinite expansion. The main challenge here is how
+to make this set complete, or at least define the constraints on possible
+recursion that guarantee it will work.
+
+\todo{Reference Christian for loop unrolling?}
+\stopitemize
+
+\section{Multiple clock domains and asynchronicity}
+Cλash currently only supports synchronous systems with a single clock domain.
+In a lot of real-world systems, both of these limitations pose problems.
+
+There might be asynchronous events to which a system wants to respond. The
+most obvious asynchronous event is of course a reset signal. Though a reset
+signal can be synchronous, that is less flexible (and a hassle to describe in
+Cλash, currently). Since every function in Cλash describes the behaviour on
+each cycle boundary, we really can't fit in asynchronous behaviour easily.
+
+Due to the same reason, multiple clock domains cannot be easily supported. There is
+currently no way for the compiler to know in which clock domain a function
+should operate and since the clock signal is never explicit, there is also no
+way to express circuits that synchronize various clock domains.
+
+A possible way to express more complex timing behaviour would be to make
+functions more generic event handlers, where the system generates a stream of
+events (Like \quote{clock up}, \quote{clock down}, \quote{input A changed},
+\quote{reset}, etc.). When working with multiple clock domains, each domain
+could get its own clock events.
+
+As an example, we would have something like the following:
+
+\starthaskell
+data Event = ClockUp | Reset | ...
+
+type MainState = State Word
+
+-- Initial state
+initstate :: MainState
+initstate = State 0
+
+main :: Word -> Event -> MainState -> (MainState, Word)
+main inp event (State acc) = (State acc', acc')
+ where
+ acc' = case event of
+ -- On a reset signal, reset the accumulator and output
+ Reset -> initstate
+ -- On a normal clock cycle, accumulate the result of func
+ ClockUp -> acc + (func inp event)
+ -- On any other event, leave state and output unchanged
+ _ -> acc
+
+-- func is some combinatoric expression
+func :: Word -> Event -> Word
+func inp _ = inp * 2 + 3
+\stophaskell
+
+\todo{Picture}
+
+In this example, we see that every function takes an input of type
+\hs{Event}. The function \hs{main} that takes the output of
+\hs{func} and accumulates it on every clock cycle. On a reset signal, the
+accumulator is reset. The function \hs{func} is just a combinatoric
+function, with no synchronous elements. We can see this because there is no
+state and the event input is completely ignored. If the compiler is smart
+enough, we could even leave the event input out for functions that don't use
+it, either because they are completely combinatoric (like in this example), or
+because they rely on the the caller to select the clock signal.
+
+This structure is similar to the event handling structure used to perform I/O
+in languages like Amanda. \todo{ref} There is a top level case expression that
+decides what to do depending on the current input event.
+
+A slightly more complex example that shows a system with two clock domains.
+There is no real integration between the clock domains (there is one input and
+one output for each clock domain), but it does show how multiple clocks can be
+distinguished.
+
+\starthaskell
+data Event = ClockUpA | ClockUpB | ...
+
+type MainState = State (SubAState, SubBState)
+
+-- Initial state
+initstate :: MainState
+initstate = State (initsubastate, initsubbstate)
+
+main :: Word -> Word -> Event -> MainState -> (MainState, Word, Word)
+main inpa inpb event (State (sa, sb)) = (State (sa', sb'), outa, outb)
+ where
+ -- Only update the substates if the corresponding clock has an up
+ -- transition.
+ sa' = case event of
+ ClockUpA -> sa''
+ _ -> sa
+ sb' = case event of
+ ClockUpB -> sb''
+ _ -> sb
+ -- Always call suba and subb, so we can always have a value for our output
+ -- ports.
+ (sa'', outa) = suba inpa sa
+ (sb'', outb) = subb inpb sb
+
+type SubAState = State ...
+suba :: Word -> SubAState -> (SubAState, Word)
+suba = ...
+
+type SubBState = State ...
+subb :: Word -> SubAState -> (SubAState, Word)
+subb = ...
+\stophaskell
+
+Note that in the above example the \hs{suba} and \hs{subb} functions are
+\emph{always} called, to get at their combinatoric outputs. The new state
+is calculated as well, but only saved when the right clock has an up
+transition.
+
+As you can see, there is some code duplication in the case statement that
+selects the right clock. One of the advantages of an explicit approach like
+this, is that some of this duplication can be extracted away into helper
+functions. For example, we could imagine a \hs{select_clock} function, which
+takes a stateful function that is not aware of events, and changes it into a
+function that only updates its state on a specific (clock) event.
+
+\starthaskell
+select_clock :: Event
+ -> (input -> State s -> (State s, output))
+ -> (input -> State s -> Event -> (State s, output))
+select_clock clock func inp state event = (state', out)
+ where
+ state' = if clock == event then state'' else state
+ (state'', out) = func inp state
+
+main :: Word -> Word -> Event -> MainState -> (MainState, Word, Word)
+main inpa inpb event (State (sa, sb)) = (State (sa', sb'), outa, outb)
+ where
+ (sa'', outa) = (select_clock ClockUpA suba) inpa sa event
+ (sb'', outb) = (select_clock ClockUpB subb) inpb sb event
+\stophaskell
+
+As you can see, this can greatly reduce the length of the main function, while
+increasing the readability. As you might also have noted, the select\_clock
+function takes any stateful function from the current Cλash prototype and
+turns it into an event-aware function!
+
+Going along this route for more complex timing behaviour seems promising,
+espicially since it seems possible to express very advanced timing behaviours,
+while still allowing simple functions without any extra overhead when complex
+behaviour is not needed.
+
+The main cost of this approach will probably be extra complexity in the
+compiler: The paths (state) data can take become very non-trivial, and it
+is probably hard to properly analyze these paths and produce the
+intended \VHDL description.
+
+\section{Multiple cycle descriptions}
+In the current Cλash prototype, every description is a single-cycle
+description. In other words, every function describes behaviour for each
+separate cycle and any recursion (or folds, maps, etc.) is expanded in space.
+
+Sometimes, you might want to have a complex description that could possibly
+take multiple cycles. Some examples include:
+
+\startitemize
+ \item Some kind of map or fold over a list that could be expanded in time
+ instead of space. This would result in a function that describes n cycles
+ instead of just one, where n is the lenght of the list.
+ \item A large combinatoric expressions that would introduce a very long
+ combinatoric path and thus limit clock frequency. Such an expression could
+ be broken up into multiple stages, which effectively results in a pipelined
+ system (see also \in{section}[sec:future:pipelining]) with a known delay.
+ There should probably be some way for the developer to specify the cycle
+ division of the expression, since automatically deciding on such a division
+ is too complex and contains too many tradeoffs, at least initially.
+ \item Unbounded recursion. It is not possible to expand unbounded (or even
+ recursion with a depth that is not known at compile time) in space, since
+ there is no way to tell how much hardware to create (it might even be
+ infinite).
+
+ When expanding infinite recursion over time, each step of the recursion can
+ simply become a single clockcycle. When expanding bounded but unknown
+ recursion, we probably need to add an extra data valid output bit or
+ something similar.
+\stopitemize
+
+Apart from translating each of these multiple cycle descriptions into a per-cycle
+description, we also need to somehow match the type signature of the multiple
+cycle description to the type signature of the single cycle description that
+the rest of the system expects (assuming that the rest of the system is
+described in the \quote{normal} per-cycle manner). For example, an infinitely
+recursive expression typically has the return type \lam{[a]}, while the rest
+of the system would expect just \lam{a} (since the recursive expression
+generates just a single element each cycle).
+
+Naively, this matching could be done using a (builtin) function with a
+signature like \lam{[a] -> a}, which also serves as an indicator to the
+compiler that some expanding over time is required. However, this poses a
+problem for simulation: How will our Haskell implementation of this magical
+builtin function know which element of the input list to return. This
+obviously depends on the current cycle number, but there is no way for this
+function to know the current cycle without breaking all kinds of safety and
+purity properties. Making this function have some state input and output could
+help, though this state is not present in the actual hardware (or perhaps
+there is some state, if there are value passed from one recursion step to the
+next, but how can the type of that state be determined by the typechecker?).
+
+It seems that this is the most pressing problem for multicycle descriptions:
+How to interface with the rest of the system, without sacrificing safety and
+simulation capabilities?
+
+\section{Higher order values in state}
+Another interesting idea is putting a higher order value inside a function's
+state value. Since we can use higher order values anywhere, why not in the
+state?
+
+As a (contrived) example, consider the following accumulator:
+
+\starthaskell
+-- The accumulator function that takes a word and returns a new accumulator
+-- and the result so far. This is the function we want to put inside the
+-- state.
+type Acc = Word -> (Acc, Word)
+acc = \a -> (\b -> acc ( a + b ), a )
+
+main :: Word -> State Acc -> (State Acc, Word)
+main a s = (State s', out)
+ where (s', out) = s a
+\stophaskell
+
+This code uses a function as its state, which implicitely contains the value
+accumulated so far. This is a fairly trivial example, that is more easy to
+write with a simple \hs{Word} state value, but for more complex descriptions
+this style might pay off. Note that in a way we are using the
+\emph{continuation passing style} of writing functions, where we pass a
+sort of \emph{continuation} from one cycle to the next.
+
+Our normalization process completely removes higher order values inside a
+function by moving applications and higher order values around so that every
+higher order value will eventually be full applied. However, if we would put a
+higher order value inside our state, the path from the higher order value
+definition to its application runs through the state, which is external to the
+function. A higher order value defined in one cycle is not applied until a
+later cycle. Our normalization process only works within the function, so it
+cannot remove this use of a higher order value.
+
+However, we cannot leave a higher order value in our state value, since it is
+impossible to generate a register containing a higher order value, we simply
+can't translate a function type to a hardware type. To solve this, we must
+replace the higher order value inside our state with some other value
+representing these higher order values.
+
+On obvious approach here is to use an algebraic datatype where each
+constructor represents one possible higher order value that can end up in the
+state and each constructor has an argument for each free variable of the
+higher order value replaced. This allows us to completely reconstruct the
+higher order value at the spot where it is applied, and thus the higher order
+value disappears.
+
+This approach is commonly known as the \quote{Reynolds approach to
+defuntionalization}, first described by J.C. Reynolds and seems to apply well
+to this situation. One note here is that Reynolds' approach puts all the
+higher order values in a single datatype. For a typed language, we will at
+least have to have a single datatype for each function type, since we can't
+mix them. It would be even better to split these datatypes a bit further, so
+that such a datatype will never hold a constructor that is never used for a
+particular state variable. This separation is probably a non-trivial problem,
+though.
+
+\todo{Reference "Definitional interpreters for higher-order programming
+languages":
+http://portal.acm.org/citation.cfm?id=805852\&dl=GUIDE\&coll=GUIDE\&CFID=58835435\&CFTOKEN=81856623}
+
+\section{New language}
+During the development of the prototype, it has become clear that Haskell is
+not the perfect language for this work. There are two main problems:
+\startitemize
+\item Haskell is not expressive enough. Haskell is still quite new in the area
+of dependent typing, something we use extensively. Also, Haskell has some
+special syntax to write monadic composition and arrow composition, which is
+well suited to normal Haskell programs. However, for our hardware
+descriptions, we could use some similar, but other, syntactic sugar (as we
+have seen above).
+\item Haskell is too expressive. There are some things that Haskell can
+express, but we can never properly translate. There are certain types (both
+primitive types and certain type constructions like recursive types) we can
+never translate, as well as certain forms of recursion.
+\stopitemize
+
+It might be good to reevaluate the choice of language for Cλash, perhaps there
+are other languages which are better suited to describe hardware, now that
+we've learned a lot about it.
+
+Perhaps Haskell (or some other language) can be extended by using a
+preprocessor. There has been some (point of proof) work on a the Strathclyde
+Haskell Enhancement (\small{SHE}) preprocessor for type-level programming,
+perhaps we can extend that, or create something similar for hardware-specific
+notation.
+
+It is not unlikely that the most flexible way
+forward would be to define a completely new language with exactly the needed
+features. This is of course an enormous effort, which should not be taken
+lightly.
+
+\section{Don't care values}
+ A powerful value in \VHDL is the \emph{don't care} value, given as
+ \type{'-'}. This value tells the compiler that you don't really care about
+ which value is assigned to a signal, allowing the compiler to make some
+ optimizations. Since hardware choice in hardware is often implemented using
+ a collection of logic gates instead of multiplexers only, synthesizers can
+ often reduce the amount of hardware needed by smartly choosing values for
+ these don't care cases.
+
+ There is not really anything comparable with don't care values in normal
+ programming languages. The closest thing is an undefined or uninitialized
+ value, though those are usually associated with error conditions.
+
+ It would be useful if Cλash also has some way to specify don't care values.
+ When looking at the Haskell typing system, there are really two ways to do
+ this:
+
+ \startitemize
+ \item Add a special don't care value to every datatype. This includes the
+ obvious \hs{Bit} type, but will also need to include every user defined
+ type. An exception can be made for vectors and product types, since those
+ can simply use the don't care values of the types they contain.
+
+ This would also require some kind of \quote{Dont careable} type class
+ that allows each type to specify what its don't care value is. The
+ compiler must then recognize this constant and replace it with don't care
+ values in the final \VHDL code.
+
+ This is of course a very intrusive solution. Every type must become member
+ of this typeclass, and there is now some member in every type that is a
+ special don't care value. Guaranteeing the obvious don't care semantics
+ also becomes harder, since every pattern match or case statement must now
+ also take care of the don't care value (this might actually be an
+ advantage, since it forces designers to specify how to handle don't care
+ for different operations).
+
+ \item Use the special \hs{undefined}, or \emph{bottom} value present in
+ Haskell. This is a type that is member of all types automatically, without
+ any explicit declarations.
+
+ Any expression that requires evaluation of an undefined value
+ automatically becomes undefined itself (or rather, there is some exception
+ mechanism). Since Haskell is lazy, this means that whenever it tries to
+ evaluate undefined, it is apparently required for determining the output
+ of the system. This property is useful, since typically a don't care
+ output is used when some output is not valid and should not be read. If
+ it is in fact not read, it should never be evaluated and simulation should
+ be fine.
+
+ In practice, this works less ideal. In particular, pattern matching is not
+ always smart enough to deal with undefined. Consider the following
+ definition of an \hs{and} operator:
+
+ \starthaskell
+ or :: Bit -> Bit -> Bit
+ and Low _ = Low
+ and _ Low = Low
+ and High High = High
+ \stophaskell
+
+ When using the \hs{and} operation on an undefined (don't care) and a Low
+ value should always return a Low value. Its value does not depend on the
+ value chosen for the don't care value. However, though when applying the
+ above and function to \hs{Low} and \hs{undefined} results in exactly that
+ behviour, the result is \hs{undefined} when the arguments are swapped.
+ This is because the first pattern forces the first argument to be
+ evaluated. If it is \hs{undefined}, evaluation is halted and an exception
+ is show, which is not what is intended.
+ \stopitemize
-Using monadic do does not fit the typing
+ These options should be explored further to see if they provide feasible
+ methods for describing don't care conditions. Possibly there are completely
+ other methods which work better.
-Using custom combinators would work
+\section{Correctness proofs of the normalization system}
+As stated in \in{section}[sec:normalization:properties], there are a
+number of properties we would like to see verified about the
+normalization system. In particular, the \emph{termination} and
+\emph{completeness} of the system would be a good candidate for future
+research. Specifying formal semantics for the Core language in
+order to verify the \emph{soundness} of the system would be an even more
+challenging task.
+% vim: set sw=2 sts=2 expandtab:
projects / matthijs / master-project / report.git / blobdiff