module HaskellFold where

mySumV1 [] = 0
mySumV1 (x:xt) = x + mySumV1 xt

myProductV1 [] = 1
myProductV1 (x:xt) = x * myProductV1 xt

myMap f [] = []
myMap f (x:xt) = f x : myMap f xt

myFoldr :: (a -> b -> b) -> b -> [a] -> b
myFoldr op z [] = z
myFoldr op z (x:xt) = op x (myFoldr op z xt)

-- So here are mySumV1, myProductV1, myMap re-expressed as foldr's:
mySumFoldr xs = foldr (+) 0 xs
myProductFoldr xs = foldr (*) 1 xs
myMapFoldr f xs = foldr (\x r -> f x : r) [] xs


mySumV2 xs = g 0 xs
  where
    -- If you want to use induction to prove g, use this specification:
    -- for all xs, for all a, g a xs = a + sum of xs

    g accum [] = accum
    
    -- Induction step: The list is x:xt
    -- Induction hypothesis: for all a, g a xt = a + sum of xt
    --
    -- How to compute accum + sum of (x:xt)?
    --
    --   accum + sum of (x:xt)
    -- = accum + x + sum of xt
    -- = (accum + x) + sum of xt
    -- = g (accum + x) xt               by IH
    g accum (x:xt) = g (accum + x) xt

myReverse xs = g [] xs
  where
    -- If you want to use induction, the specification is:
    -- for all xs, for all a, g a xs = (reversal of xs) ++ a

    g accum [] = accum

    -- Induction step: The list is x:xt
    -- IH: for all a: g a xt = (reversal of xt) ++ a
    --
    -- How to compute (reversal of (x:xt)) ++ accum ?
    --
    --   (reversal of (x:xs)) ++ accum
    -- = (reversal of xt) ++ [x] ++ accum
    -- = (reversal of xt) ++ ([x] ++ accum)
    -- = g ([x] ++ accum) xt                    by IH
    -- = g (x : accum) xt
    g accum (x:xt) = g (x : accum) xt

myFoldl op z [] = z
myFoldl op z (x:xs) = myFoldl op (op z x) xs

mySumFoldl xs = myFoldl (+) 0 xs

myReverseFoldl xs = myFoldl (flip (:)) [] xs