module Data.Sized.Internal
(Sized(..), instLL, instFunctor, ListLikeF,
withListLikeF, withListLikeF', givenListLikeF,
givenListLikeF') where
import Data.Constraint
import Data.Constraint.Forall (Forall, inst)
import Data.Foldable (Foldable)
import Data.ListLike (FoldableLL (..), ListLike)
import qualified Data.ListLike as LL
import Data.Proxy
import qualified Data.Sequence as Seq
import Data.Traversable (Traversable)
import Data.Type.Natural (Nat)
import Data.Typeable (Typeable)
import qualified Data.Vector as V
newtype Sized f (n :: Nat) a =
Sized { runSized :: f a
} deriving (Eq, Ord, Typeable,
Functor, Foldable, Traversable)
instance ListLikeF f => FoldableLL (Sized f n a) a where
foldl f a = givenListLikeF' $ LL.foldl f a
foldl' f a = givenListLikeF' $ LL.foldl' f a
foldl1 f = givenListLikeF' $ LL.foldl1 f
foldr f a = givenListLikeF' $ LL.foldr f a
foldr' f a = givenListLikeF' $ LL.foldr' f a
foldr1 f = givenListLikeF' $ LL.foldr1 f
instance Show (f a) => Show (Sized f n a) where
showsPrec d (Sized x) = showsPrec d x
class (ListLike (f a) a) => LLF f a
instance (ListLike (f a) a) => LLF f a
instance Class (ListLike (f a) a) (LLF f a) where
cls = Sub Dict
instance (LLF f a) :=> (ListLike (f a) a) where
ins = Sub Dict
type ListLikeF f = (Functor f, Forall (LLF f))
instLLF :: forall f a. Forall (LLF f) :- ListLike (f a) a
instLLF = trans ins inst
instLL :: forall f a. ListLikeF f :- ListLike (f a) a
instLL = trans instLLF weaken2
instFunctor :: ListLikeF f :- Functor f
instFunctor = weaken1
givenListLikeF :: ListLikeF f => ((Functor f, ListLike (f a) a) => f a -> b) -> f a -> b
givenListLikeF = withListLikeF Proxy
givenListLikeF' :: ListLikeF f => ((Functor f, ListLike (f a) a) => f a -> b) -> Sized f n a -> b
givenListLikeF' f = givenListLikeF f . runSized
withListLikeF :: forall pxy f a b. ListLikeF f
=> pxy (f a) -> ((Functor f, ListLike (f a) a) => b) -> b
withListLikeF _ b = b \\ llDic &&& instFunctor
where
llDic = instLL :: ListLikeF f :- ListLike (f a) a
withListLikeF' :: ListLikeF f => f a -> ((Functor f, ListLike (f a) a) => b) -> b
withListLikeF' xs = withListLikeF (toProxy xs)
toProxy :: a -> Proxy a
toProxy = const Proxy
instance Class (FoldableLL f a) (ListLike f a) where
cls = Sub Dict
instance ListLike f a :=> FoldableLL f a where
ins = Sub Dict