{-# Language ViewPatterns, GADTs, KindSignatures #-}
import Data.List

{-
catamorphisms: folds
anamorphisms: unfolds

foldr vs foldl: foldl is almost never the right thing to use, use foldl' instead, which is a strict version
(optimiser will do this for us)
-}

foldr2 :: (a -> b -> b) -> b -> [a] -> b
foldr2 f b [] = b
foldr2 f b (h:t) = f h (foldr2 f b t)

-- easy to visualise with the list tree: it replaces the cons nodes (:) with f and nil ([]) with b

foldr3 :: ((a, b) -> b, () -> b) -> [a] -> b
foldr3 (f, b) [] = b ()
foldr3 (f, b) (h:t) = f (h, foldr3 (f, b) t)

{-
-- these two functions correspond to list type constructors:
-- data List a = Cons a (List a) -- (a, b) -> b
--             | Nil             -- ()     -> b


this view lets us generalise folds. What's the "shape" of list type?
- 2 alternatives
- in 1st, there are two values combined
- in 2nd, empty

it's a sum of products.
Products are modelled using tuples: (a, List a)
Unions are modelled using Either, so:

type List' a = Either () (a, List' a)

1:2:3:4:[]
R (1, R(2, R(3, R(4, L ()))))

these two things are isomorphic.

-}

foldr4 :: (Either (a, b) () -> b) -> [a] -> b
foldr4 f [] = f $ Right ()
foldr4 f (h:t) = f $ Left (h, foldr4 f t)

-- a simple equivalence that lets us use a single function that combines the two cases above

-- aside: turning a pair of functions into function of Either:

pair2either :: (a -> c, b -> c) -> Either a b -> c
pair2either (f, g) (Left a) = f a
pair2either (f, g) (Right b) = g b

{-
but why are we doing this? To generalise foldr to our own data type.
All we need is generalise the type of the function; we should always be able to represent the shape of our ADT
as Eithers and pairs, and then have appropriate cases

if we have multiple data constructors -> nest eithers
if we have more than two types in a product -> nest pairs


But this is not all; we can unfold lists:
-}

stars :: Int -> String
stars = unfoldr go
  where
  	go :: Int -> Maybe (Char, Int)
  	go 0 = Nothing
  	go n = Just ('*', n - 1)

-- this can be generalised as well by switching to paris and eithers!

unfoldr2 :: (b -> Either (a, b) ()) -> b -> [a]
unfoldr2 f (f -> Right ())                   = []
unfoldr2 f (f -> Left  (h, unfoldr2 f -> t)) = (h:t)

{-
(this uses view pattern: f -> x says that before pattern matching we apply f to x and pattern match on the result)
note that this is the inverse of foldr4

-}

stars2 :: Int -> String
stars2 = unfoldr2 go
  where
  	go :: Int -> Either (Char, Int) ()
  	go 0 = Right ()
  	go n = Left ('*', n - 1)


-- if we don't care too much about that nice symmetry, we can rewrite unfoldr2 without view patterns:

unfoldr3 :: (b -> Either (a, b) ()) -> b -> [a]
unfoldr3 f b = case f b of
  Right ()      -> []
  Left  (h, b') -> case (unfoldr3 f b') of t -> (h:t)

{-
Since there is no generalisation of Either to 3, 4 etc. we have to nest them, and it gets messy.

Can we write a general unfold that works for any data type? Idea:

-- X []
-- X (:) :$ '*' :? (n - 1)

Lost? Let's try to explain, but first a quick demo of GADTs...
-}

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

data List2 :: * -> * where
	Nil2 :: List2 a
	Cons2 :: a -> List2 a -> List2 a

-- basically, GADTs provide more flexible, function-like syntax


{-

data X :: * -> * where
	X    :: a -> X a
	(:$) :: X (a -> b) -> a -> X b
	(:?) :: X (a -> b) -> s -> X b

Well, this is not gonna work, the (:?) is dodgy

let's try to work out what types we need:
X (:)                 :: X (a -> ([a] -> [a]))
X (:) :$ '*'          :: X (String -> String)
X (:) :$ '*' :? (n-1) :: X String

Hmm, we might need this:
-}

data X :: * -> * -> * -> * where
	X    :: a -> X c s a
	(:$) :: X c s (a -> b) -> a -> X c s b
	(:?) :: X c s (c -> b) -> s -> X c s b

{-
s -- the seed (Int in our case)
c -- the final type we are constructing (String)

now:

go :: Int -> X String Int String
-}

{-
Why don't we just do an ordinary anamorphism on an unfixed data type? Because we don't want to have to unfix our type!

So, we were defeated during the session, but look what Peter did on his train home:
-}

unf :: forall s c . (s -> X c s c) -> s -> c
unf f = go . f
	where
		go :: X c s b -> b
		go (X x)    = x
		go (x :$ v) = go x v
		go (x :? s) = go x (unf f s)

stars3 :: Int -> String
stars3 n = unf go n
  where
  	go :: Int -> X String Int String
  	go 0 = X []
  	go n = X (:) :$ '*' :? (n - 1)