symantic-lib/Language/Symantic/Lib/Foldable.hs

   1 {-# LANGUAGE PolyKinds #-}
   2 {-# LANGUAGE UndecidableInstances #-}
   3 {-# OPTIONS_GHC -fno-warn-orphans #-}
   4 -- | Symantic for 'Foldable'.
   5 module Language.Symantic.Lib.Foldable where
   6
   7 import Control.Applicative (Alternative)
   8 import Control.Monad (MonadPlus)
   9 import Data.Foldable (Foldable)
  10 import qualified Data.Foldable as Foldable
  11 import Prelude hiding (Foldable(..)
  12  , all, and, any, concat, concatMap
  13  , mapM_, notElem, or, sequence_)
  14
  15 import Language.Symantic
  16 import Language.Symantic.Lib.Alternative (tyAlternative)
  17 import Language.Symantic.Lib.Bool (tyBool)
  18 import Language.Symantic.Lib.Eq (tyEq)
  19 import Language.Symantic.Lib.Function (a0, b1)
  20 import Language.Symantic.Lib.Functor (f2)
  21 import Language.Symantic.Lib.Int (tyInt)
  22 import Language.Symantic.Lib.List (tyList)
  23 import Language.Symantic.Lib.Monoid (tyMonoid)
  24 import Language.Symantic.Lib.Num (tyNum)
  25 import Language.Symantic.Lib.Ord (tyOrd)
  26
  27 -- * Class 'Sym_Foldable'
  28 type instance Sym Foldable = Sym_Foldable
  29 class Sym_Foldable term where
  30         foldMap    :: Foldable f => Monoid m      => term (a -> m) -> term (f a) -> term m
  31         foldr      :: Foldable f                  => term (a -> b -> b) -> term b -> term (f a) -> term b
  32         foldr'     :: Foldable f                  => term (a -> b -> b) -> term b -> term (f a) -> term b
  33         foldl      :: Foldable f                  => term (b -> a -> b) -> term b -> term (f a) -> term b
  34         foldl'     :: Foldable f                  => term (b -> a -> b) -> term b -> term (f a) -> term b
  35         length     :: Foldable f                  => term (f a) -> term Int
  36         null       :: Foldable f                  => term (f a) -> term Bool
  37         minimum    :: Foldable f => Ord a         => term (f a) -> term a
  38         maximum    :: Foldable f => Ord a         => term (f a) -> term a
  39         elem       :: Foldable f => Eq  a         => term a -> term (f a) -> term Bool; infix 4 `elem`
  40         sum        :: Foldable f => Num a         => term (f a) -> term a
  41         product    :: Foldable f => Num a         => term (f a) -> term a
  42         toList     :: Foldable f                  => term (f a) -> term [a]
  43         all        :: Foldable f                  => term (a -> Bool) -> term (f a) -> term Bool
  44         and        :: Foldable f                  => term (f Bool) -> term Bool
  45         any        :: Foldable f                  => term (a -> Bool) -> term (f a) -> term Bool
  46         concat     :: Foldable f                  => term (f [a]) -> term [a]
  47         concatMap  :: Foldable f                  => term (a -> [b]) -> term (f a) -> term [b]
  48         find       :: Foldable f                  => term (a -> Bool) -> term (f a) -> term (Maybe a)
  49         foldlM     :: Foldable f => Monad m       => term (b -> a -> m b) -> term b -> term (f a) -> term (m b)
  50         foldrM     :: Foldable f => Monad m       => term (a -> b -> m b) -> term b -> term (f a) -> term (m b)
  51         forM_      :: Foldable f => Monad m       => term (f a) -> term (a -> m b) -> term (m ())
  52         for_       :: Foldable f => Applicative p => term (f a) -> term (a -> p b) -> term (p ())
  53         mapM_      :: Foldable f => Monad m       => term (a -> m b) -> term (f a) -> term (m ())
  54         maximumBy  :: Foldable f                  => term (a -> a -> Ordering) -> term (f a) -> term a
  55         minimumBy  :: Foldable f                  => term (a -> a -> Ordering) -> term (f a) -> term a
  56         notElem    :: Foldable f => Eq a          => term a -> term (f a) -> term Bool
  57         or         :: Foldable f                  => term (f Bool) -> term Bool
  58         sequenceA_ :: Foldable f => Applicative p => term (f (p a)) -> term (p ())
  59         sequence_  :: Foldable f => Monad m       => term (f (m a)) -> term (m ())
  60         traverse_  :: Foldable f => Applicative p => term (a -> p b) -> term (f a) -> term (p ())
  61         asum       :: Foldable f => Alternative p => term (f (p a)) -> term (p a)
  62         msum       :: Foldable f => MonadPlus p   => term (f (p a)) -> term (p a)
  63
  64         default foldMap    :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monoid m       => term (a -> m) -> term (f a) -> term m
  65         default foldr      :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> b -> b) -> term b -> term (f a) -> term b
  66         default foldr'     :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> b -> b) -> term b -> term (f a) -> term b
  67         default foldl      :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (b -> a -> b) -> term b -> term (f a) -> term b
  68         default foldl'     :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (b -> a -> b) -> term b -> term (f a) -> term b
  69         default length     :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (f a) -> term Int
  70         default null       :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (f a) -> term Bool
  71         default minimum    :: Sym_Foldable (UnT term) => Trans term => Foldable f => Ord a          => term (f a) -> term a
  72         default maximum    :: Sym_Foldable (UnT term) => Trans term => Foldable f => Ord a          => term (f a) -> term a
  73         default elem       :: Sym_Foldable (UnT term) => Trans term => Foldable f => Eq  a          => term a -> term (f a) -> term Bool
  74         default sum        :: Sym_Foldable (UnT term) => Trans term => Foldable f => Num a          => term (f a) -> term a
  75         default product    :: Sym_Foldable (UnT term) => Trans term => Foldable f => Num a          => term (f a) -> term a
  76         default toList     :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (f a) -> term [a]
  77         default all        :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> Bool) -> term (f a) -> term Bool
  78         default and        :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (f Bool) -> term Bool
  79         default any        :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> Bool) -> term (f a) -> term Bool
  80         default concat     :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (f [a]) -> term [a]
  81         default concatMap  :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> [b]) -> term (f a) -> term [b]
  82         default find       :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> Bool) -> term (f a) -> term (Maybe a)
  83         default foldlM     :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m        => term (b -> a -> m b) -> term b -> term (f a) -> term (m b)
  84         default foldrM     :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m        => term (a -> b -> m b) -> term b -> term (f a) -> term (m b)
  85         default forM_      :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m        => term (f a) -> term (a -> m b) -> term (m ())
  86         default for_       :: Sym_Foldable (UnT term) => Trans term => Foldable f => Applicative p  => term (f a) -> term (a -> p b) -> term (p ())
  87         default mapM_      :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m        => term (a -> m b) -> term (f a) -> term (m ())
  88         default maximumBy  :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> a -> Ordering) -> term (f a) -> term a
  89         default minimumBy  :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (a -> a -> Ordering) -> term (f a) -> term a
  90         default notElem    :: Sym_Foldable (UnT term) => Trans term => Foldable f => Eq a           => term a -> term (f a) -> term Bool
  91         default or         :: Sym_Foldable (UnT term) => Trans term => Foldable f                   => term (f Bool) -> term Bool
  92         default sequenceA_ :: Sym_Foldable (UnT term) => Trans term => Foldable f => Applicative p  => term (f (p a)) -> term (p ())
  93         default sequence_  :: Sym_Foldable (UnT term) => Trans term => Foldable f => Monad m        => term (f (m a)) -> term (m ())
  94         default traverse_  :: Sym_Foldable (UnT term) => Trans term => Foldable f => Applicative p  => term (a -> p b) -> term (f a) -> term (p ())
  95         default asum       :: Sym_Foldable (UnT term) => Trans term => Foldable f => Alternative m  => term (f (m a)) -> term (m a)
  96         default msum       :: Sym_Foldable (UnT term) => Trans term => Foldable f => MonadPlus m    => term (f (m a)) -> term (m a)
  97
  98         foldMap    = trans2 foldMap
  99         foldr      = trans3 foldr
 100         foldr'     = trans3 foldr'
 101         foldl      = trans3 foldl
 102         foldl'     = trans3 foldl'
 103         length     = trans1 length
 104         null       = trans1 null
 105         minimum    = trans1 minimum
 106         maximum    = trans1 maximum
 107         elem       = trans2 elem
 108         sum        = trans1 sum
 109         product    = trans1 product
 110         toList     = trans1 toList
 111         all        = trans2 all
 112         and        = trans1 and
 113         any        = trans2 any
 114         concat     = trans1 concat
 115         concatMap  = trans2 concatMap
 116         find       = trans2 find
 117         foldlM     = trans3 foldlM
 118         foldrM     = trans3 foldrM
 119         forM_      = trans2 forM_
 120         for_       = trans2 for_
 121         mapM_      = trans2 mapM_
 122         maximumBy  = trans2 maximumBy
 123         minimumBy  = trans2 minimumBy
 124         notElem    = trans2 notElem
 125         or         = trans1 or
 126         sequenceA_ = trans1 sequenceA_
 127         sequence_  = trans1 sequence_
 128         traverse_  = trans2 traverse_
 129         asum       = trans1 asum
 130         msum       = trans1 msum
 131
 132 -- Interpreting
 133 instance Sym_Foldable Eval where
 134         foldMap    = eval2 Foldable.foldMap
 135         foldr      = eval3 Foldable.foldr
 136         foldr'     = eval3 Foldable.foldr'
 137         foldl      = eval3 Foldable.foldl
 138         foldl'     = eval3 Foldable.foldl'
 139         null       = eval1 Foldable.null
 140         length     = eval1 Foldable.length
 141         minimum    = eval1 Foldable.minimum
 142         maximum    = eval1 Foldable.maximum
 143         elem       = eval2 Foldable.elem
 144         sum        = eval1 Foldable.sum
 145         product    = eval1 Foldable.product
 146         toList     = eval1 Foldable.toList
 147         all        = eval2 Foldable.all
 148         and        = eval1 Foldable.and
 149         any        = eval2 Foldable.any
 150         concat     = eval1 Foldable.concat
 151         concatMap  = eval2 Foldable.concatMap
 152         find       = eval2 Foldable.find
 153         foldlM     = eval3 Foldable.foldlM
 154         foldrM     = eval3 Foldable.foldrM
 155         forM_      = eval2 Foldable.forM_
 156         for_       = eval2 Foldable.for_
 157         mapM_      = eval2 Foldable.mapM_
 158         maximumBy  = eval2 Foldable.maximumBy
 159         minimumBy  = eval2 Foldable.minimumBy
 160         notElem    = eval2 Foldable.notElem
 161         or         = eval1 Foldable.or
 162         sequenceA_ = eval1 Foldable.sequenceA_
 163         sequence_  = eval1 Foldable.sequence_
 164         traverse_  = eval2 Foldable.traverse_
 165         asum       = eval1 Foldable.asum
 166         msum       = eval1 Foldable.msum
 167 instance Sym_Foldable View where
 168         foldMap    = view2 "foldMap"
 169         foldr      = view3 "foldr"
 170         foldr'     = view3 "foldr'"
 171         foldl      = view3 "foldl"
 172         foldl'     = view3 "foldl'"
 173         null       = view1 "null"
 174         length     = view1 "length"
 175         minimum    = view1 "minimum"
 176         maximum    = view1 "maximum"
 177         elem       = view2 "elem"
 178         sum        = view1 "sum"
 179         product    = view1 "product"
 180         toList     = view1 "toList"
 181         all        = view2 "all"
 182         and        = view1 "and"
 183         any        = view2 "any"
 184         concat     = view1 "concat"
 185         concatMap  = view2 "concatMap"
 186         find       = view2 "find"
 187         foldlM     = view3 "foldlM"
 188         foldrM     = view3 "foldrM"
 189         forM_      = view2 "forM_"
 190         for_       = view2 "for_"
 191         mapM_      = view2 "mapM_"
 192         maximumBy  = view2 "maximumBy"
 193         minimumBy  = view2 "minimumBy"
 194         notElem    = view2 "notElem"
 195         or         = view1 "or"
 196         sequenceA_ = view1 "sequenceA_"
 197         sequence_  = view1 "sequence_"
 198         traverse_  = view2 "traverse_"
 199         asum       = view1 "asum"
 200         msum       = view1 "msum"
 201 instance (Sym_Foldable r1, Sym_Foldable r2) => Sym_Foldable (Dup r1 r2) where
 202         foldMap    = dup2 @Sym_Foldable foldMap
 203         foldr      = dup3 @Sym_Foldable foldr
 204         foldr'     = dup3 @Sym_Foldable foldr'
 205         foldl      = dup3 @Sym_Foldable foldl
 206         foldl'     = dup3 @Sym_Foldable foldl'
 207         null       = dup1 @Sym_Foldable null
 208         length     = dup1 @Sym_Foldable length
 209         minimum    = dup1 @Sym_Foldable minimum
 210         maximum    = dup1 @Sym_Foldable maximum
 211         elem       = dup2 @Sym_Foldable elem
 212         sum        = dup1 @Sym_Foldable sum
 213         product    = dup1 @Sym_Foldable product
 214         toList     = dup1 @Sym_Foldable toList
 215         all        = dup2 @Sym_Foldable all
 216         and        = dup1 @Sym_Foldable and
 217         any        = dup2 @Sym_Foldable any
 218         concat     = dup1 @Sym_Foldable concat
 219         concatMap  = dup2 @Sym_Foldable concatMap
 220         find       = dup2 @Sym_Foldable find
 221         foldlM     = dup3 @Sym_Foldable foldlM
 222         foldrM     = dup3 @Sym_Foldable foldrM
 223         forM_      = dup2 @Sym_Foldable forM_
 224         for_       = dup2 @Sym_Foldable for_
 225         mapM_      = dup2 @Sym_Foldable mapM_
 226         maximumBy  = dup2 @Sym_Foldable maximumBy
 227         minimumBy  = dup2 @Sym_Foldable minimumBy
 228         notElem    = dup2 @Sym_Foldable notElem
 229         or         = dup1 @Sym_Foldable or
 230         sequenceA_ = dup1 @Sym_Foldable sequenceA_
 231         sequence_  = dup1 @Sym_Foldable sequence_
 232         traverse_  = dup2 @Sym_Foldable traverse_
 233         asum       = dup1 @Sym_Foldable asum
 234         msum       = dup1 @Sym_Foldable msum
 235
 236 -- Transforming
 237 instance (Sym_Foldable term, Sym_Lambda term) => Sym_Foldable (BetaT term)
 238
 239 -- Typing
 240 instance NameTyOf Foldable where
 241         nameTyOf _c = ["Foldable"] `Mod` "Foldable"
 242 instance FixityOf Foldable
 243 instance ClassInstancesFor Foldable
 244 instance TypeInstancesFor Foldable
 245
 246 -- Compiling
 247 instance Gram_Term_AtomsFor src ss g Foldable
 248 instance (Source src, SymInj ss Foldable) => ModuleFor src ss Foldable where
 249         moduleFor = ["Foldable"] `moduleWhere`
 250          [ "foldMap" := teFoldable_foldMap
 251          , "foldr"   := teFoldable_foldr
 252          , "foldr'"  := teFoldable_foldr'
 253          , "foldl"   := teFoldable_foldl
 254          , "elem" `withInfixN` 4 := teFoldable_elem
 255          , "sum"     := teFoldable_sum
 256          , "product" := teFoldable_product
 257          , "toList"  := teFoldable_toList
 258          , "all"     := teFoldable_all
 259          , "any"     := teFoldable_any
 260          , "and"     := teFoldable_and
 261          , "or"      := teFoldable_or
 262          , "concat"  := teFoldable_concat
 263          , "asum"    := teFoldable_asum
 264          -- , "msum"    := teFoldable_msum
 265          ]
 266
 267 -- ** 'Type's
 268 tyFoldable :: Source src => Type src vs a -> Type src vs (Foldable a)
 269 tyFoldable a = tyConstLen @(K Foldable) @Foldable (lenVars a) `tyApp` a
 270
 271 t0 :: Source src => LenInj vs => KindInj (K t) =>
 272       Type src (Proxy t ': vs) t
 273 t0 = tyVar "t" $ varZ
 274
 275 t1 :: Source src => LenInj vs => KindInj (K t) =>
 276       Type src (a ': Proxy t ': vs) t
 277 t1 = tyVar "t" $ VarS varZ
 278
 279 t2 :: Source src => LenInj vs => KindInj (K t) =>
 280       Type src (a ': b ': Proxy t ': vs) t
 281 t2 = tyVar "t" $ VarS $ VarS varZ
 282
 283 -- ** 'Term's
 284 teFoldable_foldMap :: TermDef Foldable '[Proxy a, Proxy t, Proxy m] (Foldable t # Monoid m #> ((a -> m) -> t a -> m))
 285 teFoldable_foldMap = Term (tyFoldable t1 # tyMonoid m) ((a0 ~> m) ~> t1 `tyApp` a0 ~> m) $ teSym @Foldable $ lam2 foldMap
 286         where
 287         m :: Source src => LenInj vs => KindInj (K m) =>
 288              Type src (a ': b ': Proxy m ': vs) m
 289         m = tyVar "m" $ VarS $ VarS varZ
 290
 291 teFoldable_elem :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t # Eq a #> (a -> t a -> Bool))
 292 teFoldable_elem = Term (tyFoldable t1 # tyEq a0) (a0 ~> t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam2 elem
 293
 294 teFoldable_toList :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t a -> [a]))
 295 teFoldable_toList = Term (tyFoldable t1) (t1 `tyApp` a0 ~> tyList a0) $ teSym @Foldable $ lam1 toList
 296
 297 teFoldable_concat :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t [a] -> [a]))
 298 teFoldable_concat = Term (tyFoldable t1) (t1 `tyApp` (tyList a0) ~> tyList a0) $ teSym @Foldable $ lam1 concat
 299
 300 teFoldable_foldr, teFoldable_foldr' :: TermDef Foldable '[Proxy a, Proxy b, Proxy t] (Foldable t #> ((a -> b -> b) -> b -> t a -> b))
 301 teFoldable_foldr = Term (tyFoldable t2) ((a0 ~> b1 ~> b1) ~> b1 ~> t2 `tyApp` a0 ~> b1) $ teSym @Foldable $ lam3 foldr
 302
 303 teFoldable_foldr' = Term (tyFoldable t2) ((a0 ~> b1 ~> b1) ~> b1 ~> t2 `tyApp` a0 ~> b1) $ teSym @Foldable $ lam3 foldr'
 304
 305 teFoldable_foldl :: TermDef Foldable '[Proxy a, Proxy b, Proxy t] (Foldable t #> ((b -> a -> b) -> b -> t a -> b))
 306 teFoldable_foldl = Term (tyFoldable t2) ((b1 ~> a0 ~> b1) ~> b1 ~> t2 `tyApp` a0 ~> b1) $ teSym @Foldable $ lam3 foldl
 307
 308 teFoldable_length :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t a -> Int))
 309 teFoldable_length = Term (tyFoldable t1) (t1 `tyApp` a0 ~> tyInt) $ teSym @Foldable $ lam1 length
 310
 311 teFoldable_null :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t a -> Bool))
 312 teFoldable_null = Term (tyFoldable t1) (t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam1 null
 313
 314 teFoldable_minimum, teFoldable_maximum :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t # Ord a #> (t a -> a))
 315 teFoldable_minimum = Term (tyFoldable t1 # tyOrd a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 minimum
 316 teFoldable_maximum = Term (tyFoldable t1 # tyOrd a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 maximum
 317
 318 teFoldable_sum, teFoldable_product :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t # Num a #> (t a -> a))
 319 teFoldable_sum = Term (tyFoldable t1 # tyNum a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 sum
 320 teFoldable_product = Term (tyFoldable t1 # tyNum a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 product
 321
 322 teFoldable_all, teFoldable_any :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> ((a -> Bool) -> t a -> Bool))
 323 teFoldable_all = Term (tyFoldable t1) ((a0 ~> tyBool) ~> t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam2 all
 324 teFoldable_any = Term (tyFoldable t1) ((a0 ~> tyBool) ~> t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam2 any
 325
 326 teFoldable_and, teFoldable_or :: TermDef Foldable '[Proxy t] (Foldable t #> (t Bool -> Bool))
 327 teFoldable_and = Term (tyFoldable t0) (t0 `tyApp` tyBool ~> tyBool) $ teSym @Foldable $ lam1 and
 328 teFoldable_or = Term (tyFoldable t0) (t0 `tyApp` tyBool ~> tyBool) $ teSym @Foldable $ lam1 or
 329
 330 teFoldable_asum :: TermDef Foldable '[Proxy a, Proxy t, Proxy f] ((Foldable t # Alternative f) #> (t (f a) -> f a))
 331 teFoldable_asum = Term (tyFoldable t1 # tyAlternative f2) (t1 `tyApp` (f2 `tyApp` a0) ~> (f2 `tyApp` a0)) $ teSym @Foldable $ lam1 asum
 332
 333 {- TODO: when MonadPlus will be supported
 334 teFoldable_msum ::
 335  Source src => SymInj ss Foldable =>
 336  Term src ss ts '[Proxy a, Proxy t, Proxy f] ((Foldable t # MonadPlus f) #> (t (f a) -> f a))
 337 teFoldable_msum =
 338         Term ((tyFoldable t1 # (tyConst @(K MonadPlus) @MonadPlus `tyApp` f2))) (t1 `tyApp` (f2 `tyApp` a0) ~> (f2 `tyApp` a0)) $
 339         teSym @Foldable $ lam1 msum
 340 -}