Ex3_4.hs

import Prelude hiding (last, (!!), map, id)

{-@ Induction examples from slide @-}

data Foo a = Nil | Cons  a (Foo a)
--    ^       ^    ^
--    |       |    |
--   type    data constructor
--  constructor

-- data FooF = NilF | ConsF Float FooF

-- foo = Cons 5 (Cons 3 Nil)
-- foo1 = Cons 5.3 Nil
-- foof = ConsF 5.3 NilF

{-@

data List a  = Nil | Cons a (List a)


Cons 1 (Cons 2 (Cons 3 Nil))

1 `Cons` 2 `Cons` 3 `Cons` Nil -- infix

1 : 2 : 3 : []

[1, 2, 3] = 1 : 2 : 3 : []
              ^          ^
              |          |
             Cons       Nil
foo :: [a] ->......
foo (x : xs) = .......
x = 1; xs = [2, 3]
foo [1, 2, 3]


@-}

{-@

Parametric Polymorphism -- a -> a
Ad-hoc Polymorphism -- Typeclasses

@-}


id :: a -> a -- Permissive
id x = x     -- Restrictive
-- last [1, 2, 3] = 3

-- Partial
last :: [a] -> a
last [x] = x
last (_ : xs) = last xs

-- | Partial vs Total Function

-- | Can you define a Haskell datatype for which `last` is total?

-- data Maybe a = Nothing | Just a
-- (!!) :: [a] -> Int -> Maybe a
-- xs !! n = if (length xs < n)
--           then Nothing
--           else Just (xs !!! n)
--                where

(!!) :: [a] -> Int -> a
xs     !! n | n < 0 =  error "negative index"
[]     !! _ =  error "index too large"
(x:_)  !! 0 =  x
(_:xs) !! n =  xs !! (n-1)

-- | Write a total version of (!!)
(!!!) :: [a] -> Int -> Maybe a
[] !!! _  = Nothing
(x:xs) !!! 0  = Just x
(x : xs)  !!! n = xs !!! (n - 1)



{-@ Higher order function @-}

map :: (a -> b) -> [a] -> [b]
map _ [] = []
map f (x:xs) = f x : map f xs

-- | doubles [[1,2], [3,4], [5,6]] == [[2,4], [6,8], [10,12]]

doubles :: [[Int]] -> [[Int]]
doubles = map (map (* 2))

-- | doubleSecond [(1, 2), (2, 4)] == [(1, 4), (2, 8)]
doubleSecond :: Functor f => f (a, Int) -> f (a, Int)
doubleSecond = fmap (fmap (* 2))

{-@ Lambda syntax and fold @-}
-- | intercalate ", " ["A","B","C"] = "A, B, C"
intercalate :: [a] -> [[a]]-> [a]
-- intercalate sep (x:xss) = foldl (\acc y -> acc ++ sep ++ y) x xss
intercalate sep xss = foldr (\x acc -> if null acc
                                           then x
                                           else x ++ sep ++ acc) [] xss


squares :: [Int]
squares = [x * x | x <- [1..5]]

pairs :: [(Int, Int)]
pairs = [(x, y) | x <- [1..3], y <- [1..3]]

{-@ Pascal's Triangle and List Comprehension @-}

pascal :: [[Int]]
pascal = [[ choose r c | c <- [0..r]] | r <- [0..]]

choose :: Int -> Int -> Int
choose _ 0 = 1
choose n k
  | n == k = 1
choose n k = pascal !! (n - 1) !! k + pascal !! (n - 1) !! (k - 1)


{-@ Folds - An abstraction over recursion @-}


all :: (a -> Bool) -> [a] -> Bool
all p = foldr (\x acc -> p x && acc) True

any :: (a -> Bool) -> [a] -> Bool
any p = foldr (\x acc -> p x || acc) False

Proofs.agda

{- PROOF MECHANISATION
   -------------------
   How do I know that my proofs are correct?


   Agda proofs have the form
   begin
      p1
   ≡⟨⟩
      p2
   ≡⟨⟩
      p3
   ∎

   Important tools: reflexivity, congruence, symmetric

   Induction based proofs typically use congruence.

   A relation is said to be a congruence for a given function if it is
   preserved by applying that function. If e is evidence that `x ≡ y`, then
   `cong f e` is evidence that `f x ≡ f y`, for any function `f`

   written as
     p1
   ≡⟨cong f (Induction hypothesis) ⟩
     p2

   Apart from that Agda is a syntactic cousin of Haskell. However, it heavily
   uses Unicode syntax as it is a tool to do formal mathematics.

   Curry-Howard Isomorphism

   Types      <->     Propositions
   Programs   <->     Proofs
   Recursion  <->     Induction

-}



_++_ : ∀ {A : Set} → List A → List A → List A
[]       ++ ys  =  ys
(x ∷ xs) ++ ys  =  x ∷ (xs ++ ys)


-- | Ex 1.
++-assoc : ∀ {A : Set} (xs ys zs : List A)
  → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc [] ys zs =
  begin
    ([] ++ ys) ++ zs
  ≡⟨⟩
    ys ++ zs
  ≡⟨⟩
    [] ++ (ys ++ zs)
  ∎
++-assoc (x ∷ xs) ys zs =
  begin
    ((x ∷ xs) ++ ys) ++ zs
  ≡⟨⟩
    (x ∷ (xs ++ ys)) ++ zs
  ≡⟨⟩
    x ∷ ((xs ++ ys) ++ zs)
  ≡⟨ cong (x ∷_) (++-assoc xs ys zs) ⟩
    x ∷ (xs ++ (ys ++ zs))
  ∎

-- | Ex 2. -- Note _⊗_("\"ox) is the variable name and _∷_ is the constructor

{- foldr in Haskell

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr _ acc []     = acc
foldr f acc (x:xs) = f x (foldr f acc xs)

-}

foldr : ∀ {A B : Set} → (A → B → B) → B → List A → B
foldr _⊗_ e []        =  e
foldr _⊗_ e (x ∷ xs)  =  x ⊗ foldr _⊗_ e xs

foldr-∷ : ∀ {A : Set} → (xs : List A)
  → foldr _∷_ [] xs ≡ xs
foldr-∷ [] = refl
foldr-∷ (x ∷ xs) =
  begin
    foldr _∷_ [] (x ∷ xs)
  ≡⟨⟩
    x ∷ foldr _∷_ [] xs
  ≡⟨ cong (x ∷_) (foldr-∷ xs) ⟩
    x ∷ xs
  ∎


-- Ex 3.

rev : ∀ {A : Set} → List A → List A
rev [] = []
rev (x ∷ xs) = rev xs ++ [ x ]

qrev : ∀ {A : Set} → List A → List A → List A
qrev [] ys = ys
qrev (x ∷ xs) ys = qrev xs (x ∷ ys)


qrev-lemma0 : ∀ {A : Set} → (xs ys zs : List A) →
  qrev xs ys ++ zs ≡ qrev xs (ys ++ zs)
qrev-lemma0 [] ys zs = refl
qrev-lemma0 (x ∷ xs) ys zs =
  begin
    qrev (x ∷ xs) ys ++ zs
  ≡⟨⟩
    qrev xs (x ∷ ys) ++ zs
  ≡⟨ qrev-lemma0 xs (x ∷ ys) zs ⟩
    qrev xs ((x ∷ ys) ++ zs)
  ≡⟨⟩
    qrev (x ∷ xs) (ys ++ zs)
  ∎

rev-qrev : ∀ {A : Set} → (xs : List A)
  → rev xs ≡ qrev xs []
rev-qrev [] =
  begin
    rev []
  ≡⟨⟩
    []
  ≡⟨⟩
    qrev [] []
  ∎
rev-qrev (x ∷ xs) =
  begin
    rev (x ∷ xs)
  ≡⟨⟩
    rev xs ++ [ x ]
  ≡⟨ cong (_++ [ x ]) (rev-qrev xs) ⟩
    qrev xs [] ++ [ x ]
  ≡⟨⟩
    qrev xs [] ++ (x ∷ [])
  ≡⟨ qrev-lemma0 xs [] (x ∷ []) ⟩
    qrev xs ([] ++ (x ∷ []))
  ≡⟨⟩
    qrev xs (x ∷ [])
  ≡⟨⟩
    qrev (x ∷ xs) []
  ∎