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, 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 (Proxy 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 FixityOf Foldable
 241 instance ClassInstancesFor Foldable
 242 instance TypeInstancesFor Foldable
 243
 244 -- Compiling
 245 instance Gram_Term_AtomsFor src ss g Foldable
 246 instance (Source src, Inj_Sym ss Foldable) => ModuleFor src ss Foldable where
 247         moduleFor = ["Foldable"] `moduleWhere`
 248          [ "foldMap" := teFoldable_foldMap
 249          , "foldr"   := teFoldable_foldr
 250          , "foldr'"  := teFoldable_foldr'
 251          , "foldl"   := teFoldable_foldl
 252          , "elem" `withInfixN` 4 := teFoldable_elem
 253          , "sum"     := teFoldable_sum
 254          , "product" := teFoldable_product
 255          , "toList"  := teFoldable_toList
 256          , "all"     := teFoldable_all
 257          , "any"     := teFoldable_any
 258          , "and"     := teFoldable_and
 259          , "or"      := teFoldable_or
 260          , "concat"  := teFoldable_concat
 261          , "asum"    := teFoldable_asum
 262          -- , "msum"    := teFoldable_msum
 263          ]
 264
 265 -- ** 'Type's
 266 tyFoldable :: Source src => Type src vs a -> Type src vs (Foldable a)
 267 tyFoldable a = tyConstLen @(K Foldable) @Foldable (lenVars a) `tyApp` a
 268
 269 t0 :: Source src => Inj_Len vs => Inj_Kind (K t) =>
 270       Type src (Proxy t ': vs) t
 271 t0 = tyVar "t" $ varZ
 272
 273 t1 :: Source src => Inj_Len vs => Inj_Kind (K t) =>
 274       Type src (a ': Proxy t ': vs) t
 275 t1 = tyVar "t" $ VarS varZ
 276
 277 t2 :: Source src => Inj_Len vs => Inj_Kind (K t) =>
 278       Type src (a ': b ': Proxy t ': vs) t
 279 t2 = tyVar "t" $ VarS $ VarS varZ
 280
 281 -- ** 'Term's
 282 teFoldable_foldMap :: TermDef Foldable '[Proxy a, Proxy t, Proxy m] (Foldable t # Monoid m #> ((a -> m) -> t a -> m))
 283 teFoldable_foldMap = Term (tyFoldable t1 # tyMonoid m) ((a0 ~> m) ~> t1 `tyApp` a0 ~> m) $ teSym @Foldable $ lam2 foldMap
 284         where
 285         m :: Source src => Inj_Len vs => Inj_Kind (K m) =>
 286              Type src (a ': b ': Proxy m ': vs) m
 287         m = tyVar "m" $ VarS $ VarS varZ
 288
 289 teFoldable_elem :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t # Eq a #> (a -> t a -> Bool))
 290 teFoldable_elem = Term (tyFoldable t1 # tyEq a0) (a0 ~> t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam2 elem
 291
 292 teFoldable_toList :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t a -> [a]))
 293 teFoldable_toList = Term (tyFoldable t1) (t1 `tyApp` a0 ~> tyList a0) $ teSym @Foldable $ lam1 toList
 294
 295 teFoldable_concat :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t [a] -> [a]))
 296 teFoldable_concat = Term (tyFoldable t1) (t1 `tyApp` (tyList a0) ~> tyList a0) $ teSym @Foldable $ lam1 concat
 297
 298 teFoldable_foldr, teFoldable_foldr' :: TermDef Foldable '[Proxy a, Proxy b, Proxy t] (Foldable t #> ((a -> b -> b) -> b -> t a -> b))
 299 teFoldable_foldr = Term (tyFoldable t2) ((a0 ~> b1 ~> b1) ~> b1 ~> t2 `tyApp` a0 ~> b1) $ teSym @Foldable $ lam3 foldr
 300
 301 teFoldable_foldr' = Term (tyFoldable t2) ((a0 ~> b1 ~> b1) ~> b1 ~> t2 `tyApp` a0 ~> b1) $ teSym @Foldable $ lam3 foldr'
 302
 303 teFoldable_foldl :: TermDef Foldable '[Proxy a, Proxy b, Proxy t] (Foldable t #> ((b -> a -> b) -> b -> t a -> b))
 304 teFoldable_foldl = Term (tyFoldable t2) ((b1 ~> a0 ~> b1) ~> b1 ~> t2 `tyApp` a0 ~> b1) $ teSym @Foldable $ lam3 foldl
 305
 306 teFoldable_length :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t a -> Int))
 307 teFoldable_length = Term (tyFoldable t1) (t1 `tyApp` a0 ~> tyInt) $ teSym @Foldable $ lam1 length
 308
 309 teFoldable_null :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> (t a -> Bool))
 310 teFoldable_null = Term (tyFoldable t1) (t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam1 null
 311
 312 teFoldable_minimum, teFoldable_maximum :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t # Ord a #> (t a -> a))
 313 teFoldable_minimum = Term (tyFoldable t1 # tyOrd a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 minimum
 314 teFoldable_maximum = Term (tyFoldable t1 # tyOrd a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 maximum
 315
 316 teFoldable_sum, teFoldable_product :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t # Num a #> (t a -> a))
 317 teFoldable_sum = Term (tyFoldable t1 # tyNum a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 sum
 318 teFoldable_product = Term (tyFoldable t1 # tyNum a0) (t1 `tyApp` a0 ~> a0) $ teSym @Foldable $ lam1 product
 319
 320 teFoldable_all, teFoldable_any :: TermDef Foldable '[Proxy a, Proxy t] (Foldable t #> ((a -> Bool) -> t a -> Bool))
 321 teFoldable_all = Term (tyFoldable t1) ((a0 ~> tyBool) ~> t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam2 all
 322 teFoldable_any = Term (tyFoldable t1) ((a0 ~> tyBool) ~> t1 `tyApp` a0 ~> tyBool) $ teSym @Foldable $ lam2 any
 323
 324 teFoldable_and, teFoldable_or :: TermDef Foldable '[Proxy t] (Foldable t #> (t Bool -> Bool))
 325 teFoldable_and = Term (tyFoldable t0) (t0 `tyApp` tyBool ~> tyBool) $ teSym @Foldable $ lam1 and
 326 teFoldable_or = Term (tyFoldable t0) (t0 `tyApp` tyBool ~> tyBool) $ teSym @Foldable $ lam1 or
 327
 328 teFoldable_asum :: TermDef Foldable '[Proxy a, Proxy t, Proxy f] ((Foldable t # Alternative f) #> (t (f a) -> f a))
 329 teFoldable_asum = Term (tyFoldable t1 # tyAlternative f2) (t1 `tyApp` (f2 `tyApp` a0) ~> (f2 `tyApp` a0)) $ teSym @Foldable $ lam1 asum
 330
 331 {- TODO: when MonadPlus will be supported
 332 teFoldable_msum ::
 333  Source src => Inj_Sym ss Foldable =>
 334  Term src ss ts '[Proxy a, Proxy t, Proxy f] ((Foldable t # MonadPlus f) #> (t (f a) -> f a))
 335 teFoldable_msum =
 336         Term ((tyFoldable t1 # (tyConst @(K MonadPlus) @MonadPlus `tyApp` f2))) (t1 `tyApp` (f2 `tyApp` a0) ~> (f2 `tyApp` a0)) $
 337         teSym @Foldable $ lam1 msum
 338 -}