content: \section{A syntax for (complex) arithmetical expressions}
  \label{sec:complex-arithmetic}
  
  By following \citet{adams2010calculus}, we have arrived at
  a representation which captures the \emph{\addtoindex{semantics}} of
  complex numbers.
  %
  This kind of representation is often called a ``\addtoindex{shallow
    embedding}''.
  %
  Now we turn to the study of the \emph{\addtoindex{syntax}} instead
  (``\addtoindex{deep embedding}'').
  %
  We collect these syntactic definitions in a separate module which
  imports the earlier semantic definitions:
  %
  \begin{code}
  module DSLsofMath.ComplexSyn where
  import DSLsofMath.CSem (Complex(C), addC, mulC, Ring)
  import DSLsofMath.ComplexSem
  \end{code}
  %
  \index{AST||see {abstract syntax tree}}%
  %
  We want a datatype |ComplexE| for the \addtoindex{abstract syntax
    tree} (AST) of expressions (a DSL for complex arithmetical
  expressions).
  %
  \index{DSL!complex expressions}%
  %
  The syntactic expressions can later be evaluated to semantic values:
  %
  \index{eval@@|eval : Syn -> Sem|}%
  %
  \begin{code}
  evalE :: ComplexE -> ComplexD
  \end{code}
  %
  The concept of ``an evaluator'', a function from the syntax to the
  semantics, is something we will return to many times in this
  \course{}.
  %
  The datatype |ComplexE| should collect ways of building syntactic
  expressions representing complex numbers and we have so far seen
  %
  the symbol |i|, an embedding from |REAL|, addition and multiplication.
  %
  \index{constructor function}%
  %
  We make these four operations into \emph{constructors} in one
  recursive datatype as follows:
  %
  %format I2 = I
  \begin{code}
  data ComplexE  =  I2
                 |  ToComplex REAL
                 |  Add   ComplexE  ComplexE
                 |  Mul  ComplexE  ComplexE
   deriving (Eq, Show)
  \end{code}
  \index{deriving@@|deriving| (keyword)}%
  \index{Eq@@|Eq| (type class)}%
  %
  Note that, in |ComplexA| above, we also had a constructor for
  addition (|CPlus1|), but it was playing a different role.
  %
  They are distinguished by type: |CPlus1| took two real numbers as
  arguments, while |Add| here takes two complex expressions as
  arguments.
  
  Here are two examples of type |ComplexE| as Haskell code and as
  ASTs:
  \begin{code}
  testE1 = Mul I2 I2
  testE2 = Add (ToComplex 3) (Mul (ToComplex 2) I2)
  \end{code}
  
  \hspace{2em}
  \begin{tikzpicture}[level 1/.style={sibling distance=3cm},baseline]
  \node{|Mul|}
  child {node {|I2|}}
  child {node {|I2|}};
  \end{tikzpicture}
  \hspace{2em}
  \begin{tikzpicture}[level 1/.style={sibling distance=3cm},baseline]
  \node{|Add|}
  child {node {|ToComplex|} child {node {|3|}}}
  child {node {|Mul|}
    child {node {|ToComplex|} child {node {|2|}}}
    child {node {|I2|}}};
  \end{tikzpicture}
  
  We can implement the evaluator |evalE| by pattern matching on the
  constructors of the syntax tree and by recursion.
  %
  To write a recursive function requires a small leap of faith.
  %
  It can be difficult to get started implementing a function (like
  |evalE|) that should handle all the cases and all the levels of a
  recursive datatype (like |ComplexE|).
  %
  One way to overcome this difficulty is through what may seem at first
  glance ``\addtoindex{wishful thinking}'': assume that all but one case
  have been implemented already.
  %
  All you need to do is to focus on that one remaining case, and you can
  freely call the function (that you are implementing) recursively, as
  long as you do it for subexpressions (subtrees of the abstract syntax
  tree datatype).
  %
  This pattern is called \emph{\addtoindex{structural induction}}.
  
  For example, when implementing the |evalE (Add c1 c2)| case, you can
  assume that you already know the values |s1, s2 :: ComplexD|
  corresponding to the subtrees |c1| and |c2| of type |ComplexE|.
  %
  The only thing left is to add them up componentwise and we can assume
  there is a function |addD :: ComplexD -> ComplexD -> ComplexD| taking
  care of this step (in fact, we implemented it earlier in
  \refSec{sec:complexcase}).
  %
  Continuing in this direction (by structural induction; or ``wishful
  thinking'') we arrive at the following implementation:
  %
  \begin{code}
  evalE I2              = iD
  evalE (ToComplex r)   = toComplexD r
  evalE (Add  c1 c2)    = addD  (evalE c1)  (evalE c2)
  evalE (Mul  c1 c2)    = mulD  (evalE c1)  (evalE c2)
  \end{code}
  %
  Note the pattern here: for each constructor of the syntax datatype we
  assume that there exists a corresponding semantic function.
  %
  The next step is to implement these functions, but let us first list
  their types and compare them with the types of the syntactic constructors:
  %
  \begin{spec}
  I2   :: ComplexE
  iD   :: ComplexD
  
  ToComplex   :: REAL -> ComplexE
  toComplexD  :: REAL -> ComplexD
  
  Mul       :: ComplexE  -> ComplexE  -> ComplexE
  mulD      :: ComplexD  -> ComplexD  -> ComplexD
  \end{spec}
  %addD   :: ComplexD -> ComplexD -> ComplexD  -- |ComplexE -> ComplexE -> ComplexE|
  As we can see, each use of |ComplexE| has been replaced be a use of
  |ComplexD|.
  %
  Finally, we can start filling in the implementations:
  %
  \begin{code}
  iD            = CD (0 ,  1)
  toComplexD r  = CD (r ,  0)
  \end{code}
  %
  The function |addD| was defined earlier and |mulD| is left as an
  exercise for the reader.
  %
  To sum up we have now implemented a recursive datatype for
  mathematical expressions describing complex numbers, and an evaluator
  that computes the underlying number.
  %
  Note that many different syntactic expressions will evaluate to the
  same number (|evalE| is not injective).
  
  Generalising from the example of |testE2| we also define a function to
  embed a semantic complex number in the syntax:
  %
  \begin{code}
  fromCD :: ComplexD -> ComplexE
  fromCD (CD (x , y)) = Add (ToComplex x) (Mul (ToComplex y) I2)
  \end{code}
  %
  This function is injective: different complex numbers map to different
  syntactic expressions.
  
  \section{Laws, properties and testing}
  There are certain laws that we would like to hold for operations on complex
  numbers.
  %
  To specify these laws, in a way which can be easily testable in
  Haskell, we use functions to |Bool| (also called
  \emph{\addtoindex{predicate}s} or \emph{properties}).
  %
  The intended meaning of such a Boolean function (representing a law)
  is ``for all inputs, this should return |True|''.
  %
  This idea is at the core of \emph{\addtoindex{property based testing}}
  (pioneered by \citet{claessen_quickcheck_2000}) and conveniently
  available in the Haskell library QuickCheck.
  %
  \index{QuickCheck||see {property based testing}}%
  
  Note that a predicate |p : A -> Bool| can also be used to specify the
  \addtoindex{subset} of |A| for which |p| returns |True|.
  %
  QuickCheck is very good at finding \addtoindex{counterexample}s to
  candidate laws: values for which |p| returns |False|.
  %
  With the subset interpretation this means that QuickCheck helps
  finding elements in the set specified by the opposite predicate |not
  . p : A -> Bool|.
  %
  When it fails, we hope that the set of counterexamples is actually
  empty, but we cannot know that for sure without a proof (or by
  exhaustive testing of all cases).
  
  %
  The simplest law is perhaps |square i = -1| from the start of
  \refSec{sec:complexcase},
  %
  \begin{code}
  propI2 :: Bool
  propI2 =  Mul I2 I2 === ToComplex (-1)
  \end{code}
  %
  Note that we use a new operator here, |(===)|.
  %
  Indeed, we reserve the usual equality |(==)| for syntactic equality
  (and here the left-hand side (LHS) is clearly not syntactically equal
  to the right-hand side).
  %
  \index{semantic equality}%
  The new operator |(===)| corresponds to semantic equality, that is,
  equality \emph{after evaluation}:
  %
  
  %{
  %format .=. = ===
  \begin{code}
  (.=.) :: ComplexE -> ComplexE -> Bool
  z .=. w {-"\quad"-} = {-"\quad"-} evalE z == evalE w
  \end{code}
  %}
  
  %if false
  Unfortunately we have not explained classes yet.
  \begin{code}
  infix 0 ===
  class SemEq a where
    (===) :: a -> a -> Bool
  instance SemEq Int where
    (===) = (==)
  instance SemEq Double where
    (===) = (==)
  instance SemEq ComplexE where
    (===) = (.=.)
  \end{code}
  %endif
  
  Another law is that |fromCD| is an embedding: if we start from a
  semantic value, embed it back into syntax, and evaluate that syntax we
  get back to the value we started from.
  %
  \begin{code}
  propFromCD :: ComplexD -> Bool
  propFromCD s =  evalE (fromCD s) == s
  \end{code}
  
  Other desirable laws are that |(+)| and |(*)| should be
  \addtoindex{associative} and \addtoindex{commutative} and |(*)| should
  \addtoindex{distribute over} |(+)|:
  %if false
  \begin{code}
  propAssocAdd    :: (Num a, SemEq a) => a -> a -> a -> Bool
  propDistMulAdd  :: (Num a, SemEq a) => a -> a -> a -> Bool
  \end{code}
  %endif
  \begin{code}
  propCommAdd     x y                = {-"\quad"-}  x + y          ===  y + x
  propCommMul     x y                = {-"\quad"-}  x * y          ===  y * x
  propAssocAdd    x y z              = {-"\quad"-}  (x + y) + z    ===  x + (y + z)
  propAssocMul    x y z              =              (x * y) * z    ===  x * (y * z)
  propDistMulAdd  x y z {-"\quad"-}  =              x * (y + z)    ===  (x * y) + (x * z)
  \end{code}
  
  These laws actually fail, but not due to any mistake in the
  implementation of |evalE| in itself.
  %
  To see this, let us consider associativity at different types:
  
  \begin{code}
  propAssocInt     = propAssocAdd ::  Int     -> Int     -> Int     -> Bool
  propAssocDouble  = propAssocAdd ::  Double  -> Double  -> Double  -> Bool
  \end{code}
  %
  The first property is fine, but the second fails.
  %
  Why?
  %
  QuickCheck can be used to find small examples --- this one is perhaps
  the best one:
  %
  \begin{code}
  notAssocEvidence :: (Double , Double , Double , Bool)
  notAssocEvidence = (lhs , rhs , lhs-rhs , lhs==rhs)
    where  lhs = (1+1)+1/3
           rhs =  1+(1+1/3)
  \end{code}
  %
  For completeness: these are the values:
  %
  \begin{spec}
    (  2.3333333333333335     -- Notice the five at the end
    ,  2.333333333333333,     -- which is not present here.
    ,  4.440892098500626e-16  -- The (very small) difference
    ,  False)
  \end{spec}
  %
  We can now see the underlying reason why some of the laws failed for
  complex numbers: the approximative nature of |Double|.
  %
  Therefore, to ascertain that there is no other bug hiding, we need to
  move away from the implementation of |REAL| as |Double|.
  %
  We do this by abstraction: we make one more version of the complex
  number type, which is parameterised on the underlying representation
  type for~|REAL|.
  %
  At the same time, to reduce the number of constructors, we combine
  |I2| and |ToComplex| to |ToComplexCart|, which corresponds to
  the primitive form |a + bi| discussed above:
  %*TODO: perhaps explain more about the generalisation step.
  
  %TODO: Add as an exercise the version with I | ToComplex | Add ... | Mul ...
  % See data blackboard/W1/20170116_114608.jpg, eval blackboard/W1/20170116_114613.jpg
  \label{sec:toComplexSyn}
  \begin{code}
  data ComplexSyn r  =  ToComplexCart r r
                     |  ComplexSyn r  :+:  ComplexSyn r
                     |  ComplexSyn r  :*:  ComplexSyn r
  
  toComplexSyn :: Num a => a -> ComplexSyn a
  toComplexSyn x = ToComplexCart x 0
  \end{code}
  %
  From Appendix~\ref{app:CSem} we import |newtype Complex r = C (r ,
  r) deriving Eq| and the semantic operations |addC| and |mulC|
  corresponding to |addD| and |mulD|.
  %
  \begin{code}
  evalCSyn :: Ring r => ComplexSyn r -> Complex r
  evalCSyn (ToComplexCart x y)  = C (x , y)
  evalCSyn (l  :+:  r)          = addC  (evalCSyn l)  (evalCSyn r)
  evalCSyn (l  :*:  r)          = mulC  (evalCSyn l)  (evalCSyn r)
  \end{code}
  %
  %if False
  \label{sec:firstFromInteger}
  \begin{code}
  negateCS :: Num a => ComplexSyn a -> ComplexSyn a
  negateCS = ((-1) :*:)
  absCS = error "absCS: missing constructor"
  signumCS = error "signumCS: missing constructor"
  instance Num a => Num (ComplexSyn a) where
     (+)  = (:+:)
     (*)  = (:*:)
     fromInteger = fromIntegerCS
     negate = negateCS
     abs = absCS
     signum = signumCS
  fromIntegerCS :: Num r =>  Integer -> ComplexSyn r
  fromIntegerCS = toComplexSyn . fromInteger
  \end{code}
  %endif
  
  % \begin{exercise}
  %   Add a few more operations (hint: extend |ComplexSyn| as well) and extend |eval| appropriately.
  % \end{exercise}
  
  With this parameterised type we can test the code for ``complex
  rationals'' to avoid rounding errors.
  %**TODO: add concrete example
  (The reason why maths textbooks rarely talk about complex rationals is
  because complex numbers are used to handle roots of all numbers
  uniformly, and roots are in general irrational.)
  
  %TODO: perhaps include
  % We can also state and check properties relating the semantic and the syntactic operations:
  %
  % |a + b = eval (Add (embed a) (embed b))| for all |a| and |b|.
  \subsection{Generalising laws}
  \label{sec:generalising-laws}
  Some laws appear over and over again in different mathematical
  contexts.
  %
  \index{binary (arity 2)}%
  %
  For example, binary operators are often associative or commutative, and
  sometimes one operator distributes over another.
  %
  We will work more formally with logic in \cref{sec:logic} but
  we introduce a few definitions already here:
  
  |Associative (⊛) = Forall (a, b, c) ((a⊛b)⊛c = a⊛(b⊛c))|
  
  |Commutative (⊛) = Forall (a, b) (a⊛b = b⊛a)|
  
  |Distributive (⊗) (⊕) = Forall (a, b, c) (a⊗(b⊕c) = (a⊗b)⊕(a⊗c))|
  
  \index{parameterised laws}%
  %
  The above laws are \emph{parameterised} over some operators
  (|(⊛),(⊗),(⊕)|).
  %
  These laws will hold for some operators, but not for others.
  %
  For example, division is not commutative; taking the average of two
  quantities is commutative but not associative.
  %
  (See also \crefatpage{distributivity-as-homomorphism} for further
  analysis of distributivity.)
  %
  Such generalisations can be reflected in QuickCheck properties as well.
  
  \begin{code}
  propAssoc :: SemEq a => (a -> a -> a) -> a -> a -> a -> Bool
  propAssoc (⊛) x y z =  (x ⊛ y) ⊛ z === x ⊛ (y ⊛ z)
  \end{code}
  %
  Note that |propAssoc| is a higher-order function: it takes a function
  |(⊛)| (declared as a binary operator) as its first parameter, and
  tests if it is associative.
  %
  The property is also \addtoindex{polymorphic}: it works for many
  different types |a| (all types which have an |===| operator).
  
  Thus we can specialise it to |Add|, |Mul| and any other binary
  operator, and obtain some of the earlier laws (|propAssocAdd|,
  |propAssocMul|).
  %
  The same can be done with distributivity.
  %
  Doing so we learnt that the underlying set matters: |(+)| for |REAL|
  has some properties, but |(+)| for |Double| has others.
  %
  When formalising maths as DSLs, \addtoindex{approximation} is sometimes
  convenient, but makes many laws false.
  %
  Thus, we should attempt to do it late, and if possible, leave a
  parameter to make the degree of approximation tunable (|Int|,
  |Integer|, |Float|, |Double|, |QQ|, syntax trees, etc.).
  %
  For the curious, some of our more advanced material about testing and
  different kinds of polymorphism is available in \citep{%
    DBLP:conf/esop/BernardyJC10,% {Testing Polymorphic Properties},
    DBLP:conf/types/IonescuJ11,% {Testing versus proving in climate impact research}
    DBLP:conf/haskell/JeuringJA12% {Testing type class laws}
  }.
  %**TODO: hide or give hints / method (otherwise too hard and a bit off topic)
  %Exercise: Find some operator |(#)| which satisfies |Distributive (+) (#)|
  % Answer: |max|
  
  %It is a good exercise to find other pairs of operators satisfying
  %distributive laws.
  
  %if False
  \section{Some helper functions (can be skipped)}
  \begin{code}
  -- mulD :: ComplexD -> ComplexD -> ComplexD
  mulD (CD (ar, ai)) (CD (br, bi)) = CD (ar*br - ai*bi, ar*bi + ai*br)
  
  instance Show ComplexD where
    show = showCD
  
  showCD :: ComplexD -> String
  showCD (CD (x, y)) = show x ++ " + " ++ show y ++ "i"
  
  propAssocAdd2 :: (SemEq a, Num a) => a -> a -> a -> Bool
  propAssocAdd2 = propAssoc (+)
  \end{code}
  %endif
  
  % end of formatting "bi" as just that (and not as \(b_i\)).
  %}
  
  