Adding a new exercise and solution to Section 5.1

src/Solutions/DataTypes.idr

@@ -204,9 +204,11 @@ lastMaybe (x :: Nil) = Just x
 lastMaybe (_ :: xs)  = lastMaybe xs
 
 initMaybe : List a -> Maybe (List a)
-initMaybe Nil        = Nothing
-initMaybe (x :: Nil) = Just Nil
-initMaybe (x :: xs)  = mapMaybe (x ::) (initMaybe xs)
+initMaybe l = case l of
+  Nil => Nothing
+  x :: xs => case initMaybe xs of
+    Nothing => Just Nil
+    Just ys => Just (x :: ys)
 
 foldList : (acc -> el -> acc) -> acc -> List el -> acc
 foldList fun vacc Nil       = vacc

src/Solutions/Functions2.idr

@@ -69,7 +69,25 @@ handleRequest xs (MkRequest (MkCredentials e pw) album) =
       else if elem album albums then Success album
       else                           AccessDenied e album
 
--- 2
+--2
+
+namespace Ex2
+
+  data Failure : Type where
+    UnknownUser : Email -> Failure
+    InvalidPassword : Failure
+    AccessDenied : Email -> Album -> Failure
+
+  handleRequest : DB -> Request -> Either Failure Album
+  handleRequest db req = case find ((==) req.credentials.email . email) db of
+    Nothing => Left (UnknownUser req.credentials.email)
+    Just u2 => case (u2.email == req.credentials.email && u2.password == req.credentials.password) of
+      False => Left InvalidPassword
+      True => case elem req.album u2.albums of
+        False => Left (AccessDenied req.credentials.email req.album)
+        True => Right req.album
+
+-- 3
 data Nucleobase = Adenine | Cytosine | Guanine | Thymine
 
 readBase : Char -> Maybe Nucleobase
@@ -79,7 +97,7 @@ readBase 'G' = Just Guanine
 readBase 'T' = Just Thymine
 readBase c   = Nothing
 
--- 3
+-- 4
 traverseList : (a -> Maybe b) -> List a -> Maybe (List b)
 traverseList _ []        = Just []
 traverseList f (x :: xs) =
@@ -89,14 +107,14 @@ traverseList f (x :: xs) =
       Nothing => Nothing
     Nothing => Nothing
 
--- 4
+-- 5
 DNA : Type
 DNA = List Nucleobase
 
 readDNA : String -> Maybe DNA
 readDNA = traverseList readBase . unpack
 
--- 5
+-- 6
 complement : DNA -> DNA
 complement = map comp
   where comp : Nucleobase -> Nucleobase

src/Tutorial/Functions2.md

@@ -353,7 +353,19 @@ available in the *Prelude* (check out its type!).
    `handleRequest`. This should allow you to completely get rid
    of the `where` block.
 
-2. Define an enumeration type listing the four
+2. Refactor `handleRequest` to use `Either`, such that
+   `handleRequest : DB -> Request -> Either Failure Album`, where
+
+   ```idris
+   data Failure : Type where
+     UnknownUser : Email -> Failure
+     InvalidPassword : Failure
+     AccessDenied : Email -> Album -> Failure
+   ```
+
+   Hint: You may find nested `case` statements helpful.
+
+3. Define an enumeration type listing the four
    [nucleobases](https://en.wikipedia.org/wiki/Nucleobase)
    occurring in DNA strands. Define also a type alias
    `DNA` for lists of nucleobases.
@@ -363,7 +375,7 @@ available in the *Prelude* (check out its type!).
    `'A'`, `'a'`. Note, that this function might fail, so adjust the
    result type accordingly.
 
-3. Implement the following function, which tries to convert all
+4. Implement the following function, which tries to convert all
    values in a list with a function, which might fail. The
    result should be a `Just` holding the list of converted
    values in unmodified order, if and
@@ -376,11 +388,11 @@ available in the *Prelude* (check out its type!).
    You can verify, that the function behaves correctly with
    the following test: `traverseList Just [1,2,3] = Just [1,2,3]`.
 
-4. Implement function `readDNA : String -> Maybe DNA`
+5. Implement function `readDNA : String -> Maybe DNA`
    using the functions and types defined in exercises 2 and 3.
    You will also need function `unpack` from the *Prelude*.
 
-5. Implement function `complement : DNA -> DNA` to
+6. Implement function `complement : DNA -> DNA` to
    calculate the complement of a strand of DNA.
 
 ## The Truth about Function Arguments