open import Logic
open import Nat
open import Eq
open import Bool
open import Maybe
open import Decide
open import List
open import Vec

{-

  Fun with Agda -- Getting rid of your booleans

                Ulf Norell

-}
module Talk where

{-
  Why do we want to get rid of booleans?

  * Correctness? Booleans are error prone, but that's not really my motivation.
  
  * More informative types helps when
    - writing the program: telling the type checker what you want to do
                           means that it's in a position to help you rather
                           than simply complaining when you make mistakes
    - reading the program: more informative types makes it easier to see up
                           front what a function is doing and (as we'll see)
                           can make the definition easier to read.

-}

-- Here's an example: to figure out what this function is doing you have to
-- spend a few seconds looking through the definition.
badlyNamed :  {A}  (A  A  Bool)  List A  List A  Bool
badlyNamed _==_ []       ys       = true
badlyNamed _==_ (x  xs) []       = false
badlyNamed _==_ (x  xs) (y  ys) = (x == y) && badlyNamed _==_ xs ys

-- Here's a more informative return type for the function above.
-- Informally it says: xs is a prefix of ys precisely when ys is of the form xs ++ zs
-- and the witness for that is zs.
data Prefix {A n} (xs : Vec A n) :  {m}  Vec A m  Set where
  prefix :  {m} (zs : Vec A m)  Prefix xs (xs ++ zs)

-- Now we can read off what the function is doing just looking at the type.
isPrefixOf :  {A n m}  ((x y : A)  Maybe (x  y)) 
               (xs : Vec A n) (ys : Vec A m)  Maybe (Prefix xs ys)
isPrefixOf _==_ []       ys = just (prefix ys)
isPrefixOf _==_ (x  xs) [] = nothing
isPrefixOf _==_ (x  xs) (y  ys)           with x == y
isPrefixOf _==_ (x  xs) (y  ys)           | nothing = nothing
isPrefixOf _==_ (x  xs) (.x  ys)          | just refl with isPrefixOf _==_ xs ys
isPrefixOf _==_ (x  xs) (.x  ys)          | just refl | nothing = nothing
isPrefixOf _==_ (x  xs) (.x  .(xs ++ zs)) | just refl | just (prefix zs) =
  just (prefix zs)
-- Reading off this last equation we see that
--   isPrefixOf _==_ (x ∷ xs) (x ∷ xs ++ zs) = just (prefix zs)
-- which makes perfect sense.

-- Above we only did positive information. We can replace Maybe by Dec which contains negative
-- evidence in addition to the positive evidence we returned before.
clickDecToJumpToItsDefinition = Dec

-- We need some helper functions for constructing negative evidence.

-- If x ≠ y then x ∷ xs is not a prefix of y ∷ ys (for any xs and ys)
noHd :  {A m n}{x y : A}{xs : Vec A n}{ys : Vec A m}  ¬ x  y  ¬ Prefix (x  xs) (y  ys)
noHd prf (prefix zs) = prf refl

-- If xs is not a prefix of ys then x ∷ xs is not a prefix of y ∷ ys (for any x and y)
noTl :  {A m n}{x y : A}{xs : Vec A n}{ys : Vec A m}  ¬ Prefix xs ys  ¬ Prefix (x  xs) (y  ys)
noTl prf (prefix zs) = prf (prefix zs)

-- The new function. The positive cases stay the same but we have to do a little bit more
-- work in the negative cases. In particular in the cons cases where we have to use our
-- helper functions.
isPrefixOf′ :  {A n m}  ((x y : A)  Dec (x  y)) 
                (xs : Vec A n) (ys : Vec A m)  Dec (Prefix xs ys)
isPrefixOf′ _==_ []       ys = yes (prefix ys)
isPrefixOf′ _==_ (x  xs) [] = no λ ()
isPrefixOf′ _==_ (x  xs) (y  ys)           with x == y
isPrefixOf′ _==_ (x  xs) (y  ys)           | no np = no (noHd np)
isPrefixOf′ _==_ (x  xs) (.x  ys)          | yes refl with isPrefixOf′ _==_ xs ys
isPrefixOf′ _==_ (x  xs) (.x  ys)          | yes refl | no np           = no (noTl np)
isPrefixOf′ _==_ (x  xs) (.x  .(xs ++ zs)) | yes refl | yes (prefix zs) = yes (prefix zs)