content: -- | 
  -- Module: Data.Scoped.List
  -- This module defines a type of lists indexed by a scope
  -- The lists are homogenous, and every type in the list must be indexed
  -- by the same scope.
  -- This module is intended to be imported qualified and used with the 
  -- OverloadedLists Haskell language extension. Many of the operations 
  -- in this module have the same name as prelude functions.
  {-# LANGUAGE DerivingStrategies, DeriveAnyClass #-}
  module Data.Scoped.List (List, 
        pattern Nil, pattern (:<), 
        Data.Scoped.List.uncons,
        (Data.Scoped.List.++),
        Data.Scoped.List.concat,
        Data.Scoped.List.filter,
        Data.Scoped.List.zipWith,
        Data.Scoped.List.zipWithM_,
        IsList(..),
        module Data.Scoped.Classes) where
  
  import Data.Nat ( Nat )
  import Data.Kind ( Type )
  import GHC.IsList ( IsList(..) )
  import GHC.Generics 
  import Test.QuickCheck ( Arbitrary )
  import Control.DeepSeq ( NFData )
  import Data.Coerce ( coerce )
  import Control.Monad qualified as M
  import Data.Scoped.Classes
  
  -- | Lists where every element has type (a n)
  -- Note: the `n` is *not* the length of the list, it is a common scope 
  -- for all elements in the list.
  newtype List a n = MkList [a n] 
      deriving newtype (Eq, Ord, Read, Show, Semigroup, Monoid, Generic, Arbitrary, NFData)
      deriving anyclass (ScopedFoldable [], ScopedTraversable [], 
                          ScopedFunctor [], ScopedApplicative [], ScopedMonad [])
  
  uncons :: List a n -> Maybe (a n, List a n)
  uncons x = case coerce x of 
        [] -> Nothing
        x:xs -> Just (x,coerce xs)
  
  {-# COMPLETE (:<), Nil #-}
  pattern Nil :: forall a n. List a n
  pattern Nil <- (uncons -> Nothing)
   where 
     Nil = coerce ([] :: [a n])
  
  pattern (:<) :: a n -> List a n -> List a n
  pattern x :< xs <- (uncons -> Just (x,xs))
    where 
      x :< xs = coerce (x : coerce xs)
  
  -- * Prelude / Control.Monad list operations
  
  (++) :: forall t n. List t n -> List t n -> List t n
  (++) = coerce ((Prelude.++):: [t n] -> [t n] -> [t n])
  
  concat :: List (List t) n -> List t n
  concat = Data.Scoped.Classes.foldr (Data.Scoped.List.++) Nil
  
  filter :: (a n -> Bool) -> List a n -> List a n
  filter f = coerce (Prelude.filter f)
  
  zipWith :: (a n -> b n -> c n) -> List a n -> List b n -> List c n
  zipWith f = coerce (Prelude.zipWith f)
  
  zipWithM_ :: forall m k f1 f2 a b c n. (Applicative m) 
      => (a n -> b n -> m c) -> List a n -> List b n -> m ()
  zipWithM_ f = coerce (M.zipWithM_ f)
  
  -- | A general conversion to the standard list type.
  instance IsList (List v n) where
     type Item (List v n) = v n
  
     fromList :: [Item (List v n)] -> List v n
     fromList = coerce 
     
     toList :: List v n -> [Item (List v n)]
     toList = coerce
  
  -- | Enable generic programming for the `List` type
  -- We can't derive the `Data.Generic1` instance for `List` 
  -- using newtype deriving because the kinds differ.
  -- Therefore we need to write it by hand.
  instance Generic1 (List a :: Nat -> Type) where
     type Rep1 (List a) = 
        U1 :+: (Rec1 a :*: Rec1 (List a))
  
     from1 :: List a n -> Rep1 (List a) n
     from1 (MkList []) = L1 U1
     from1 (MkList (x:xs)) = R1 (Rec1 x :*: Rec1 (MkList xs))
  
     to1 :: Rep1 (List a) n -> List a n
     to1 (L1 U1) = MkList []
     to1 (R1 (Rec1 x :*: Rec1 (MkList xs))) = MkList (x : xs) 
  
  