(Num a, Num b) => (b,a -> a -> a -> a)

this can be read as: being a of type Num and b of type Num, then the type is (b,a -> a -> a -> a)

which is the same as saying that the type is (Num,Num -> Num -> Num -> Num)

The elements of a tuple don’t have to be of the same value.

(simple 1 2 3, simple) is a tuple composed of:
– in the first position, a value of type Num. This is a value because ‘simple 1 2 3′ contains all the inputs defined as values, so ‘simple 1 2 3′ is calculated and the result ’5′ is used instead.
– in the second position there is a function with 3 inputs and 1 output, all of type Num. In this case the inputs are not defined and thus ‘simple’ can’t be calculated, ‘simple’ is then just the definition of the function, which type is
(Num a) => a -> a -> a -> a

> evaluate :: Expr -> [(String, Float)] -> Float

instead of

> evaluate :: Expr -> Float

I would suggest

> evaluate :: Expr -> Float
> evaluate (C x) = x
> evaluate (e1 :+ e2) = evaluate e1 + evaluate e2
> evaluate (e1 :- e2) = evaluate e1 – evaluate e2
> evaluate (e1 :* e2) = evaluate e1 * evaluate e2
> evaluate (e1 :/ e2) = evaluate e1 / evaluate e2
> {- the above are the old definition given in the book -}
> evaluate (Let str val (C x)) = x
> evaluate (Let str val (exp1 :+ exp2)) = (evaluate (Let str val exp1)) + (evaluate (Let str val exp2))
> evaluate (Let str val (exp1 :- exp2)) = (evaluate (Let str val exp1)) – (evaluate (Let str val exp2))
> evaluate (Let str val (exp1 :* exp2)) = (evaluate (Let str val exp1)) * (evaluate (Let str val exp2))
> evaluate (Let str val (exp1 :/ exp2)) = (evaluate (Let str val exp1)) / (evaluate (Let str val exp2))
> evaluate (Let str val (V str2)) | str == str2 = evaluate val
> | otherwise = error (“undefined variable “++str2)

I think the late binding mechanism should keep its environment, so I suggest
> eval (Let arg e1 e2) map = eval e2 (\x->if x==arg then (C $ eval e1 map) else map x)

We include a little test program at the end.

{-
 A version of containsS for polygons which handles non-convex polygons.
 
 We compute the winding number of the polygon around the point as follows.
 For the point p and consecutive vertices a and b of the polygon (in that
 order), we have to turn from the vector PA = a-p to the vector PB = b-p.
 We wish to know the angle between these vectors, measured in an
 anticlockwise direction, and such the absolute angle is 0 <= angle <= pi.
 If the angle is pi or either PA or PB is zero, then P lies on the line
 segment AB, possibly at an endpoint.  In this case, the point is definitely
 contained within the polygon, and we need go no further.
 
 Otherwise, we proceed as follows.  We consider the plane as the complex
 plane, and write PA = a-p = z1 = x1 + i*y1,  PB = b-p = z2 = x2 + i*y2.
 Then the rotation+enlargement from PA to PB is given by
 
   z2/z1 = (x2 + i*y2) / (x1 + i*y1)
         = ( (x2 + i*y2) * (x1 - i*y1) ) / (x1^2 + y1^2)
         = ( (x1*x2 + y1*y2) + i*(x1*y2 - x2*y1) ) / (x1^2 + y1^2)
 
 Since we are only interested in the angle and not the enlargement, we
 can find this as the angle of the vector (x1*x2 + y1*y2, x1*y2 - x2*y1)
 from the origin.  This also save us from having to perform complicated
 calculations to determine whether either of PA or PB is zero; PA or PB is
 zero if both the real part (x1*x2 + y1*y2) and the imaginary part
 (x1*y2 - x2*y1) are zero, and the angle is pi if the imaginary part is
 zero and the real part is negative.
 
 We thus compute this for each pair of adjacent vertices, and return a pair
 (hit, angle), with hit==True if the point p lies on the side AB and False
 otherwise, and angle is the required angle.
 
 We use the Standard Prelude function atan2 y x which returns the angle
 from the origin to the point (x,y), measured anticlockwise from the x-axis
 and lying in the range -pi <= atan2 y x <= pi.  Note the order of the
 arguments of atan2!!
 
 Finally, if any hit is True, the point is contained within the polygon.
 Otherwise, we add up all the angles, divide the answer by 2*pi, and round
 to the nearest integer (to overcome rounding errors).  If the final answer
 is 0, then the point is outside the polygon, otherwise it is inside.
 (If the final answer is 2, it means that the polygon winds twice around this
 point, and the polygon is self-intersecting.)
-}
 
winding :: Coordinate -> Ray -> (Bool,Float)
winding (px,py) ((ax,ay),(bx,by))
  = let x1 = ax - px
        y1 = ay - py
        x2 = bx - px
        y2 = by - py
        re = x1*x2 + y1*y2
        im = x1*y2 - x2*y1
    in aux re im
       where aux r i
               | r <= 0 && i == 0  = (True,0)
               | otherwise         = (False, atan2 i r)
 
containsS :: Shape -> Coordinate -> Bool
(Rectangle s1 s2) `containsS` (x,y)
   = let t1 = s1/2; t2 = s2/2
     in (-t1<=x) && (x<=t1) && (-t2<=y) && (y<=t2)
(Ellipse r1 r2) `containsS` (x,y)
   = (x/r1)^2 + (y/r2)^2 <= 1
(Polygon pts) `containsS` p
   = let windings       = map (winding p) (zip pts (tail pts ++ [head pts]))
         (hits, angles) = unzip windings
     in or hits || round (sum angles / (2 * pi)) /= 0
(RtTriangle s1 s2) `containsS` p
   = (Polygon [(0,0),(s1,0),(0,s2)]) `containsS` p
 
shs :: [Shape]
shs = [
  Polygon [(-1,-1),(-1,1),(1,1),(1,-1)],
  Polygon [(-1,-1),(1,-1),(1,1),(-1,1)],
  Polygon [(-1,-1),(0,-1),(-1,1),(0,1)],
  Polygon [(-1,-1),(-1,1),(1,1),(1,-1),(-1,-1)],  
  Polygon [(-1,-1),(-1,1),(1,-1)],
  Polygon [(-1,-1),(-1,1),(0,0)],
  Polygon [(-1,-1),(-1,1),(0,1)]
  ]
 
shcontains = map (\x -> x `containsS` (0,0)) shs
 
main :: IO()
main = do putStrLn (show shcontains)

Unfortunately, however, the method shown does not work in this case:

let poly = Polygon ([(-1,-1),(1,-1),(1,1),(-1,1)])
    p = (0,0)
in poly `containsS'` p

gives a result of False, even though the point (0,0) clearly lies inside the square.

The reason is that the point outside that is chosen is (2,2), and the ray (0,0) to (2,2) passes through the vertex (1,1), and so lies on two edges.

This problem is therefore far subtler than it first appears.

One approach is to use the given idea but to take account of the fixed ray (from chosen point to outside point) passing through vertices, by having each one counting for 0.5. However, this will also fail if the ray just touches a vertex (if the shape is concave). A fix for this is to use signed crossings, taking account of the direction in which the rays cross. But this is getting fairly awkward and difficult.

I’m currently working on an alternative approach which uses winding numbers – we’ll see how it works out ….

Julian

r1 u r2 for r1 `Union` r2

and

r1 n r2 for r1 `Intersection` r2

Also, I will write r’ for Complement r, 0 for Empty and 1 for univ,
and a simple = sign instead of the three-line equivalence notation.

Then the five axioms, together with some simple corollaries, read:

Axiom 1
——-

r1 u (r2 u r3) = (r1 u r2) u r3
r1 n (r2 n r3) = (r1 n r2) n r3

Axiom 2
——-

r1 u r2 = r2 u r1
r1 n r2 = r2 n r1

Axiom 3
——-

r1 n (r2 u r3) = (r1 n r2) u (r1 n r3)
r1 u (r2 n r3) = (r1 u r2) n (r1 u r3)

Corollaries:

(r2 u r3) n r1 = (r2 n r1) u (r3 n r1)
(r2 n r3) u r1 = (r2 u r1) n (r3 u r1)

Proof: Apply Axiom 2 to both sides.

Axiom 4
——-

r u 0 = r
r n 1 = r

Corollaries:

0 u r = r
1 n r = r

Proof: Apply Axiom 2 to the left side.

Axiom 5
——-

r u r’ = 1
r n r’ = 0

Corollaries:

r’ u r = 1
r’ n r = 0

Proof: Apply Axiom 2 to the left side.

Now for the exercise at hand…

Lemma 1
——-

r n r = r
r u r = r

Proof:

r = r n 1 [Axiom 4]
= r n (r u r’) [Axiom 5]
= (r n r) u (r n r’) [Axiom 3]
= (r n r) u 0 [Axiom 5]
= r n r [Axiom 4]

The proof of the second statement is essentially identical, swapping
n with u and 1 with 0:

r = r u 0 [Axiom 4]
= r u (r n r’) [Axiom 5]
= (r u r) n (r u r’) [Axiom 3]
= (r u r) n 1 [Axiom 5]
= r u r [Axiom 4]

Lemma 2
——-

r u 1 = 1
r n 0 = 0

Proof:

r u 1 = r u (r u r’) [Axiom 5]
= (r u r) u r’ [Axiom 1]
= r u r’ [Lemma 1]
= 1 [Axiom 5]

and again, the other is exactly parallel:

r n 0 = r n (r n r’) [Axiom 5]
= (r n r) n r’ [Axiom 1]
= r n r’ [Lemma 1]
= 0 [Axiom 5]

Corollaries:

1 u r = 1
0 n r = 0

Proof: Apply Axiom 2 to the left side.

Lemma 3
——-

r1 u (r1 n r2) = r1
r1 n (r1 u r2) = r1

Proof (the first step is sneaky):

r1 u (r1 n r2) = (r1 n 1) u (r1 n r2) [Axiom 4]
= r1 n (1 u r2) [Axiom 3, in reverse]
= r1 n 1 [Lemma 2, corollary]
= r1 [Axiom 4]

And again, swapping n with u and 1 with 0 gives the corresponding
result:

r1 n (r1 u r2) = (r1 u 0) n (r1 u r2) [Axiom 4]
= r1 u (0 n r2) [Axiom 3, in reverse]
= r1 u 0 [Lemma 2, corollary]
= r1 [Axiom 4]

Alternatively, the latter can be deduced from the former as follows:

r1 n (r1 u r2) = (r1 n r1) u (r1 n r2) [Axiom 3]
= r1 u (r1 n r2) [Lemma 1]
= r1 [first part of Lemma 3]

Lemma 4
——-

r” = r, where r” means (r’)’

Proof:

The idea of this proof is to show that r” u r = r and also r” u r = r”,
so that r = r” u r = r”, or r” = r. It could be written in one
long chain, but it is clearer to write it in two halves.

We have

r” u r = (r” u r) n 1 [Axiom 4]
= (r” u r) n (r u r’) [Axiom 5]
= (r u r”) n (r u r’) [Axiom 2]
= r u (r” n r’) [Axiom 3, in reverse]
= r u (r’ n (r’)') [Axiom 2, and writing r''=(r')']
= r u 0 [Axiom 5]
= r [Axiom 4]

Likewise, but this time writing 1 = r’ u (r’)’ instead of 1 = r u r’,
we get:

r” u r = (r” u r) n 1 [Axiom 4]
= (r” u r) n (r’ u (r’)') [Axiom 5]
= (r” u r) n (r” u r’) [Axiom 2, and writing (r')'=r'']
= r” u (r n r’) [Axiom 3, in reverse]
= r” u 0 [Axiom 5]
= r” [Axiom 4]

Therefore r = r”.

Lemma 5
——-

0′ = 1
1′ = 0

Well, the first is the definition of univ (as given just before Axiom
3), and the proof the of second is trivial:

1′ = (0′)’ [By definition: 1 = 0']
= 0 [Lemma 4]

Lemma 6
——-

(r1 u r2)’ = r1′ n r2′
(r1 n r2)’ = r1′ u r2′

These are the famous De Morgan’s Theorems, and their proof is tricky
(and not due to me, either!). We prove a preliminary lemma first.

Lemma 7
——-

If r1′ n r2 = 0 and r1′ u r2 = 1, then r1 = r2.

Proof:

r1 = r1 u 0 [Axiom 4]
= r1 u (r1′ n r2) [Hypothesis]
= (r1 u r1′) n (r1 u r2) [Axiom 3]
= 1 n (r1 u r2) [Axiom 5]
= (r1′ u r2) n (r1 u r2) [Hypothesis]
= (r2 u r1′) n (r2 u r1) [Axiom 2]
= r2 u (r1′ n r1) [Axiom 3, in reverse]
= r2 u 0 [Axiom 5, corollary]
= r2

Proof of Lemma 6
—————-

We want to show first that (r1 u r2)’ = r1′ n r2′, so we aim to show
that ((r1 u r2)’)’ n (r1′ n r2′) = 0 and ((r1 u r2)’)’ u (r1′ n r2′)
= 1, so that (r1 u r2)’ = r1′ n r2′ by Lemma 7.

We note first that ((r1 u r2)’)’ = r1 u r2 by Lemma 4. We then have

(r1 u r2) n (r1′ n r2′)

= ((r1 u r2) n r1′) n r2′ [Axiom 1]
= ((r1 n r1′) u (r2 n r1′)) n r2′ [Axiom 3, corollary]
= (0 u (r2 n r1′)) n r2′ [Axiom 5]
= (r2 n r1′) n r2′ [Axiom 4, corollary]
= (r1′ n r2) n r2′ [Axiom 2]
= r1′ n (r2 n r2′) [Axiom 1]
= r1′ n 0 [Axiom 5]
= 0 [Lemma 2]

and

(r1 u r2) u (r1′ n r2′)
= ((r1 u r2) u r1′) n ((r1 u r2) u r2′) [Axiom 3]
= ((r2 u r1) u r1′) n ((r1 u r2) u r2′) [Axiom 2]
= (r2 u (r1 u r1′)) n (r1 u (r2 u r2′)) [Axiom 1]
= (r2 u 1 ) n (r1 u 1) [Axiom 5]
= 1 n 1 [Lemma 2]
= 1 [Axiom 4]

Thus, by Lemma 7, (r1 u r2)’ = r1′ n r2′.

For the second part of Lemma 6, we can either argue identically, or as
follows:

We have

(r1 n r2)’ = ( (r1′)’ n (r2′)’ )’ [Lemma 4]
= ( ((r1′) u (r2′))’ )’ [Lemma 6, first part]
= (r1′ u r2′)” [rewriting with fewer brackets]
= r1′ u r2′ [Lemma 4]