{-# LANGUAGE Trustworthy #-}
-- | List type-families.
--
-- For term-level reflections see [defun-sop package](https://hackage.haskell.org/package/defun-sop).
--
-- Implementation note: It would be great if first-order type families,
-- like 'Append' and 'Concat', were defined already in @base@,
-- e.g. in @Data.Type.List@ module.
-- Higher-order type families, like @Map@, obviously cannot be there
-- as they rely on the defunctorization machinery.
-- Yet, some first-order type families like 'Sequence' and 'Reverse'
-- may also be defined directly, but it's more convenient to define
-- them as special case of an higher-order type family ('Map2' and 'Foldl'
-- respectively), as that makes working with them more convenient.
--
module DeFun.List (
    -- * Append
    Append, AppendSym, AppendSym1,
    -- * Map
    Map, MapSym, MapSym1,
    -- * Concat
    Concat, ConcatSym,
    -- * ConcatMap
    ConcatMap, ConcatMapSym, ConcatMapSym1,
    -- * Map2
    Map2, Map2Sym, Map2Sym1, Map2Sym2,
    -- * Sequence
    Sequence, SequenceSym,
    -- * Foldr
    Foldr, FoldrSym, FoldrSym1, FoldrSym2,
    -- * Foldl
    Foldl, FoldlSym, FoldlSym1, FoldlSym2,
    -- * ZipWith
    ZipWith, ZipWithSym, ZipWithSym1, ZipWithSym2,
    -- * Filter
    Filter, FilterSym, FilterSym1,
    -- * Reverse
    Reverse, ReverseSym,
) where

import Prelude              (Bool (..))

import DeFun.Core
import DeFun.Function

-- $setup
-- >>> import Prelude (Bool (..), Char, Maybe (..), Int, String)
-- >>> import Data.Singletons.Bool (SBool (..))
-- >>> import Numeric.Natural (Natural)
-- >>> import DeFun
-- >>> :set -dppr-cols9999

-------------------------------------------------------------------------------
-- Append
-------------------------------------------------------------------------------

-- | List append.
--
-- >>> :kind! Append [1, 2, 3] [4, 5, 6]
-- Append [1, 2, 3] [4, 5, 6] :: [Natural]
-- = [1, 2, 3, 4, 5, 6]
--
type Append :: [a] -> [a] -> [a]
type family Append xs ys where
    Append '[]       ys = ys
    Append (x ': xs) ys = x ': Append xs ys

type AppendSym :: [a] ~> [a] ~> [a]
data AppendSym xs
type instance App AppendSym xs = AppendSym1 xs

type AppendSym1 :: [a] -> [a] ~> [a]
data AppendSym1 xs ys
type instance App (AppendSym1 xs) ys = Append xs ys

-------------------------------------------------------------------------------
-- Map
-------------------------------------------------------------------------------

-- | List map
--
-- >>> :kind! Map NotSym [True, False]
-- Map NotSym [True, False] :: [Bool]
-- = [False, True]
--
-- >>> :kind! Map (Con1 Just) [1, 2, 3]
-- Map (Con1 Just) [1, 2, 3] :: [Maybe Natural]
-- = [Just 1, Just 2, Just 3]
--
type Map :: (a ~> b) -> [a] -> [b]
type family Map f xs where
    Map f '[]    = '[]
    Map f (x:xs) = f @@ x : Map f xs

type MapSym :: (a ~> b) ~> [a] ~> [b]
data MapSym f
type instance App MapSym f = MapSym1 f

type MapSym1  :: (a ~> b) -> [a] ~> [b]
data MapSym1 f xs
type instance App (MapSym1 f) xs = Map f xs

-------------------------------------------------------------------------------
-- Concat
-------------------------------------------------------------------------------

-- | List concat
--
-- >>> :kind! Concat [ [1, 2, 3], [4, 5, 6], [7, 8, 9] ]
-- Concat [ [1, 2, 3], [4, 5, 6], [7, 8, 9] ] :: [Natural]
-- = [1, 2, 3, 4, 5, 6, 7, 8, 9]
--
type Concat :: [[a]] -> [a]
type family Concat xss where
    Concat '[] = '[]
    Concat (xs : xss) = Append xs (Concat xss)

type ConcatSym :: [[a]] ~> [a]
data ConcatSym xss
type instance App ConcatSym xss = Concat xss

-------------------------------------------------------------------------------
-- ConcatMap
-------------------------------------------------------------------------------

-- | List concatMap
type ConcatMap :: (a ~> [b]) -> [a] -> [b]
type family ConcatMap f xs where
    ConcatMap f '[]    = '[]
    ConcatMap f (x:xs) = Append (f @@ x) (ConcatMap f xs)

type ConcatMapSym :: (a ~> [b]) ~> [a] ~> [b]
data ConcatMapSym f
type instance App ConcatMapSym f = ConcatMapSym1 f

type ConcatMapSym1  :: (a ~> [b]) -> [a] ~> [b]
data ConcatMapSym1 f xs
type instance App (ConcatMapSym1 f) xs = ConcatMap f xs

-------------------------------------------------------------------------------
-- Map2
-------------------------------------------------------------------------------

-- | List binary map. I.e. 'liftA2' for lists.
--
-- Note: this is not 'ZipWith'.
--
-- >>> :kind! Map2 (Con2 '(,)) [1, 2, 3] ['x', 'y']
-- Map2 (Con2 '(,)) [1, 2, 3] ['x', 'y'] :: [(Natural, Char)]
-- = ['(1, 'x'), '(1, 'y'), '(2, 'x'), '(2, 'y'), '(3, 'x'), '(3, 'y')]
--
-- This function is a good example to highlight how to defunctionalize
-- definitions with anonymous functions.
--
-- The simple definition can be written using @concatMap@ and @map@ from
-- "Prelude":
--
-- >>> import Prelude as P (concatMap, map, (.), flip)
-- >>> let map2 f xs ys = P.concatMap (\x -> P.map (f x) ys) xs
-- >>> map2 (,) "abc" "xy"
-- [('a','x'),('a','y'),('b','x'),('b','y'),('c','x'),('c','y')]
--
-- However, to make it easier (arguably) to defunctionalize, the @concatMap@ argument
-- lambda can be written in point-free form using combinators:
--
-- >>> let map2 f xs ys = P.concatMap (P.flip P.map ys P.. f) xs
-- >>> map2 (,) "abc" "xy"
-- [('a','x'),('a','y'),('b','x'),('b','y'),('c','x'),('c','y')]
--
-- Alternatively, we could define a new "top-level" function
--
-- >>> let map2Aux f ys x = P.map (f x) ys
--
-- and use it to define @map2:
--
-- >>> let map2 f xs ys = P.concatMap (map2Aux f ys) xs
-- >>> map2 (,) "abc" "xy"
-- [('a','x'),('a','y'),('b','x'),('b','y'),('c','x'),('c','y')]
--
type Map2 :: (a ~> b ~> c) -> [a] -> [b] -> [c]
type family Map2 f xs ys where
    Map2 f xs ys = ConcatMap (CompSym2 (FlipSym2 MapSym ys) f) xs

type Map2Sym :: (a ~> b ~> c) ~> [a] ~> [b] ~> [c]
data Map2Sym f
type instance App Map2Sym f = Map2Sym1 f

type Map2Sym1 :: (a ~> b ~> c) -> [a] ~> [b] ~> [c]
data Map2Sym1 f xs
type instance App (Map2Sym1 f) xs = Map2Sym2 f xs

type Map2Sym2 :: (a ~> b ~> c) -> [a] -> [b] ~> [c]
data Map2Sym2 f xs ys
type instance App (Map2Sym2 f xs) ys = Map2 f xs ys

-------------------------------------------------------------------------------
-- Sequence
-------------------------------------------------------------------------------

-- | List sequence
--
-- >>> :kind! Sequence [[1,2,3],[4,5,6]]
-- Sequence [[1,2,3],[4,5,6]] :: [[Natural]]
-- = [[1, 4], [1, 5], [1, 6], [2, 4], [2, 5], [2, 6], [3, 4], [3, 5], [3, 6]]
--
type Sequence :: [[a]] -> [[a]]
type family Sequence xss where
    Sequence '[]         = '[ '[] ]
    Sequence (xs ': xss) = Map2 (Con2 '(:)) xs (Sequence xss)

type SequenceSym :: [[a]] ~> [[a]]
data SequenceSym xss
type instance App SequenceSym xss = Sequence xss

-------------------------------------------------------------------------------
-- Foldr
-------------------------------------------------------------------------------

-- | List right fold
--
-- Using 'Foldr' we can define a @Curry@ type family:
--
-- >>> type Curry args res = Foldr (Con2 (->)) args res
-- >>> :kind! Curry String [Int, Bool]
-- Curry String [Int, Bool] :: *
-- = Int -> Bool -> [Char]
--
type Foldr :: (a ~> b ~> b) -> b -> [a] -> b
type family Foldr f z xs where
    Foldr f z '[]      = z
    Foldr f z (x : xs) = f @@ x @@ (Foldr f z xs)

type FoldrSym :: (a ~> b ~> b) ~> b ~> [a] ~> b
data FoldrSym f
type instance App FoldrSym f = FoldrSym1 f

type FoldrSym1 :: (a ~> b ~> b) -> b ~> [a] ~> b
data FoldrSym1 f z
type instance App (FoldrSym1 f) z = FoldrSym2 f z

type FoldrSym2 :: (a ~> b ~> b) -> b -> [a] ~> b
data FoldrSym2 f z xs
type instance App (FoldrSym2 f z) xs = Foldr f z xs

-------------------------------------------------------------------------------
-- Foldl
-------------------------------------------------------------------------------

-- | List left fold
--
type Foldl :: (b ~> a ~> b) -> b -> [a] -> b
type family Foldl f z xs where
    Foldl f z '[]      = z
    Foldl f z (x : xs) = Foldl f (f @@ z @@ x) xs

type FoldlSym :: (b ~> a ~> b) ~> b ~> [a] ~> b
data FoldlSym f
type instance App FoldlSym f = FoldlSym1 f

type FoldlSym1 :: (b ~> a ~> b) -> b ~> [a] ~> b
data FoldlSym1 f z
type instance App (FoldlSym1 f) z = FoldlSym2 f z

type FoldlSym2 :: (b ~> a ~> b) -> b -> [a] ~> b
data FoldlSym2 f z xs
type instance App (FoldlSym2 f z) xs = Foldl f z xs

-------------------------------------------------------------------------------
-- ZipWith
-------------------------------------------------------------------------------

-- | Zip with
--
-- >>> :kind! ZipWith (Con2 '(,)) [1, 2, 3] ['x', 'y']
-- ZipWith (Con2 '(,)) [1, 2, 3] ['x', 'y'] :: [(Natural, Char)]
-- = ['(1, 'x'), '(2, 'y')]
--
type ZipWith :: (a ~> b ~> c) -> [a] -> [b] -> [c]
type family ZipWith f xs ys where
    ZipWith f '[] ys = '[]
    ZipWith f (x : xs) '[] = '[]
    ZipWith f (x : xs) (y : ys) = f @@ x @@ y : ZipWith f xs ys

type ZipWithSym :: (a ~> b ~> c) ~> [a] ~> [b] ~> [c]
data ZipWithSym f
type instance App ZipWithSym f = ZipWithSym1 f

type ZipWithSym1 :: (a ~> b ~> c) -> [a] ~> [b] ~> [c]
data ZipWithSym1 f xs
type instance App (ZipWithSym1 f) xs = ZipWithSym2 f xs

type ZipWithSym2 :: (a ~> b ~> c) -> [a] -> [b] ~> [c]
data ZipWithSym2 f xs ys
type instance App (ZipWithSym2 f xs) ys = ZipWith f xs ys

-------------------------------------------------------------------------------
-- Filter
-------------------------------------------------------------------------------

-- | Filter list
type Filter :: (a ~> Bool) -> [a] -> [a]
type family Filter p xs where
    Filter f '[] = '[]
    Filter f (x ': xs) = FilterAux (f @@  x) x f xs

type FilterAux :: Bool -> a -> (a ~> Bool) -> [a] -> [a]
type family FilterAux b x p xs where
    FilterAux 'True  x p xs = x ': Filter p xs
    FilterAux 'False x p xs =      Filter p xs

type FilterSym :: (a ~> Bool) ~> [a] ~> [a]
data FilterSym p
type instance App FilterSym p = FilterSym1 p

type FilterSym1  :: (a ~> Bool) -> [a] ~> [a]
data FilterSym1 p xs
type instance App (FilterSym1 p) xs = Filter p xs

-------------------------------------------------------------------------------
-- Reverse
-------------------------------------------------------------------------------

-- | Reverse list
--
-- >>> :kind! Reverse [1,2,3,4]
-- Reverse [1,2,3,4] :: [Natural]
-- = [4, 3, 2, 1]
--
type Reverse :: [a] -> [a]
type family Reverse xs where
    Reverse xs = Foldl (FlipSym1 (Con2 '(:))) '[] xs

type ReverseSym :: [a] ~> [a]
data ReverseSym xs
type instance App ReverseSym xs = Reverse xs