Refactor base library structure and port additional Haskell functions

lib/base/Haskell/Control/Applicative.agda

@@ -0,0 +1,31 @@
+module Haskell.Control.Applicative where
+
+open import Haskell.Prim
+open import Haskell.Prim.Maybe
+
+open import Haskell.Prim.Applicative public
+  renaming (module Instances to ApplicativeInstances)
+open import Haskell.Prim.Alternative public
+  renaming (module Instances to AlternativeInstances)
+open import Haskell.Data.Functor public using (_<$>_)
+open import Haskell.Data.Foldable public using (asum)
+
+
+infixl 4 _<**>_
+_<**>_ : ⦃ Applicative f ⦄ → f a → f (a → b) → f b
+_<**>_ = liftA2 (λ a f → f a)
+
+liftA : ⦃ Applicative f ⦄ → (a → b) → f a → f b
+liftA f a = pure f <*> a
+
+liftA3 : ⦃ Applicative f ⦄ → (a → b → c → d) → f a → f b → f c → f d
+liftA3 f a b c = liftA2 f a b <*> c
+
+optional : ⦃ Alternative f ⦄ → f a → f (Maybe a)
+optional v = Just <$> v <|> pure Nothing
+
+-- Omitted for now:
+-- - 'newtype Const a (b :: k) = Const { getConst :: a }'
+-- - 'newtype WrappedMonad (m :: Type -> Type) a = WrapMonad { unwrapMonad :: m a }'
+-- - 'newtype WrappedArrow (a :: Type -> Type -> Type) b c = WrapArrow { unwrapArrow :: a b c }'
+-- - 'newtype ZipList a = ZipList { getZipList :: [a] }'

lib/base/Haskell/Control/Monad.agda

@@ -2,10 +2,149 @@ module Haskell.Control.Monad where
 
 open import Haskell.Prim
 open import Haskell.Prim.Bool
-open import Haskell.Prim.Monad
-open import Haskell.Prim.String
+open import Haskell.Prim.Int
+open import Haskell.Prim.Tuple
+open import Haskell.Prim.Applicative hiding (module Instances)
+open import Haskell.Prim.Alternative hiding (module Instances)
+open import Haskell.Prim.Traversable hiding (module Instances)
+open import Haskell.Prim.Foldable hiding (module Instances)
+open import Haskell.Data.Foldable using (sequenceA₋; foldlM)
+open import Haskell.Data.List using (unzip; zipWith)
 open import Haskell.Extra.Erase
 
-guard : {{ MonadFail m }} → (b : Bool) → m (Erase (b ≡ True))
-guard True = return (Erased refl)
-guard False = fail "Guard was not True"
+open import Haskell.Prim.Functor public
+  renaming (module Instances to FunctorInstances)
+open import Haskell.Prim.Applicative public
+  using () renaming (module Instances to ApplicativeInstances)
+open import Haskell.Prim.Alternative public
+  using () renaming (module Instances to AlternativeInstances)
+open import Haskell.Prim.Monad public
+  renaming (module Instances to MonadInstances)
+open import Haskell.Prim.MonadFail public
+  renaming (module Instances to MonadFailInstances)
+open import Haskell.Prim.MonadPlus public
+  renaming (module Instances to MonadPlusInstances)
+open import Haskell.Prim.Traversable public
+  using (mapM; sequence) renaming (module Instances to TraversableInstances)
+open import Haskell.Prim.Foldable public
+  using () renaming (module Instances to FoldableInstances)
+open import Haskell.Data.Traversable public using (forM)
+open import Haskell.Data.Foldable public using (mapM₋; forM₋; sequence₋; msum)
+open import Haskell.Data.Functor public using (void)
+
+
+private variable a1 a2 a3 a4 a5 r : Type
+
+infixr 1 _=<<_ _>=>_ _<=<_
+_=<<_ : ⦃ Monad m ⦄ → (a → m b) → m a → m b
+_=<<_ = flip _>>=_
+
+_>=>_ : ⦃ Monad m ⦄ → (a → m b) → (b → m c) → a → m c
+f >=> g = λ x → f x >>= g
+
+_<=<_ : ⦃ Monad m ⦄ → (b → m c) → (a → m b) → a → m c
+_<=<_ = flip _>=>_
+
+
+join : ⦃ Monad m ⦄ → m (m a) → m a
+join x = x >>= id
+
+mfilter : ⦃ MonadPlus m ⦄ → (a → Bool) → m a → m a
+mfilter p ma = do
+  a ← ma
+  if p a then return a else mzero
+
+filterM : ⦃ Applicative m ⦄ → (a → m Bool) → List a → m (List a)
+filterM p = foldr (λ x → liftA2 (λ b → if b then (x ∷_) else id) (p x)) (pure [])
+
+mapAndUnzipM : ⦃ Applicative m ⦄ → (a → m (b × c)) → List a → m (List b × List c)
+mapAndUnzipM f xs = fmap unzip (traverse f xs)
+
+zipWithM : ⦃ Applicative m ⦄ → (a → b → m c) → List a → List b → m (List c)
+zipWithM f xs ys = sequenceA (zipWith f xs ys)
+
+zipWithM₋ : ⦃ Applicative m ⦄ → (a → b → m c) → List a → List b → m ⊤
+zipWithM₋ f xs ys = sequenceA₋ (zipWith f xs ys)
+
+foldM : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (b → a → m b) → b → t a → m b
+foldM = foldlM
+
+foldM₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (b → a → m b) → b → t a → m ⊤
+foldM₋ f a xs  = foldlM f a xs >> return tt
+
+replicateMNat : ⦃ Applicative m ⦄ → Nat → m a → m (List a)
+replicateMNat zero    _ = pure []
+replicateMNat (suc n) f = liftA2 _∷_ f (replicateMNat n f)
+
+replicateM : ⦃ Applicative m ⦄ → (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → m a → m (List a)
+replicateM cnt f = replicateMNat (intToNat cnt) f
+
+replicateMNat₋ : ⦃ Applicative m ⦄ → Nat → m a → m ⊤
+replicateMNat₋ zero    _ = pure tt
+replicateMNat₋ (suc n) f = f *> replicateMNat₋ n f
+
+replicateM₋ : ⦃ Applicative m ⦄ → (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → m a → m ⊤
+replicateM₋ cnt f = replicateMNat₋ (intToNat cnt) f
+
+
+guard : ⦃ Alternative f ⦄ → (b : Bool) → f (Erase (b ≡ True))
+guard True  = pure (Erased refl)
+guard False = empty
+
+when : ⦃ Applicative f ⦄ → (b : Bool) → ({@0 p : b ≡ True} → f ⊤) → f ⊤
+when True  f = f {refl}
+when False _ = pure tt
+
+unless : ⦃ Applicative f ⦄ → (b : Bool) → ({@0 p : b ≡ False} → f ⊤) → f ⊤
+unless True  _ = pure tt
+unless False f = f {refl}
+
+
+liftM : ⦃ Monad m ⦄ → (a1 → r) → m a1 → m r
+liftM f m1 = do
+  x1 ← m1
+  return (f x1)
+
+liftM2 : ⦃ Monad m ⦄ → (a1 → a2 → r) → m a1 → m a2 → m r
+liftM2 f m1 m2 = do
+  x1 ← m1
+  x2 ← m2
+  return (f x1 x2)
+
+liftM3 : ⦃ Monad m ⦄ → (a1 → a2 → a3 → r) → m a1 → m a2 → m a3 → m r
+liftM3 f m1 m2 m3 = do
+  x1 ← m1
+  x2 ← m2
+  x3 ← m3
+  return (f x1 x2 x3)
+
+liftM4 : ⦃ Monad m ⦄ → (a1 -> a2 -> a3 -> a4 -> r) → m a1 → m a2 → m a3 → m a4 → m r
+liftM4 f m1 m2 m3 m4 = do
+  x1 ← m1
+  x2 ← m2
+  x3 ← m3
+  x4 ← m4
+  return (f x1 x2 x3 x4)
+
+liftM5 : ⦃ Monad m ⦄ → (a1 → a2 → a3 → a4 → a5 → r) → m a1 → m a2 → m a3 → m a4 → m a5 → m r
+liftM5 f m1 m2 m3 m4 m5 = do
+  x1 ← m1
+  x2 ← m2
+  x3 ← m3
+  x4 ← m4
+  x5 ← m5
+  return (f x1 x2 x3 x4 x5)
+
+ap : ⦃ Monad m ⦄ → m (a → b) → m a → m b
+ap m1 m2 = do
+  f ← m1
+  x ← m2
+  return (f x)
+
+infixl 4 _<$!>_
+_<$!>_ : ⦃ Monad m ⦄ → (a → b) → m a → m b
+_<$!>_ = fmap
+
+
+-- Omitted for now:
+-- - 'forever :: Applicative => f -> f a -> f b'

lib/base/Haskell/Data/Foldable.agda

@@ -0,0 +1,100 @@
+module Haskell.Data.Foldable where
+
+open import Haskell.Prim
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Eq hiding (module Instances)
+open import Haskell.Prim.Ord hiding (module Instances)
+open import Haskell.Prim.Monoid hiding (module Instances)
+open import Haskell.Prim.Applicative hiding (module Instances)
+open import Haskell.Prim.Alternative hiding (module Instances)
+open import Haskell.Prim.Monad hiding (module Instances)
+open import Haskell.Prim.MonadPlus hiding (module Instances)
+
+open import Haskell.Prim.Eq public
+  using () renaming (module Instances to EqInstances)
+open import Haskell.Prim.Ord public
+  using () renaming (module Instances to OrdInstances)
+open import Haskell.Prim.Monoid public
+  using () renaming (module Instances to MonoidInstances)
+open import Haskell.Prim.Applicative public
+  using () renaming (module Instances to ApplicativeInstances)
+open import Haskell.Prim.Alternative public
+  using () renaming (module Instances to AlternativeInstances)
+open import Haskell.Prim.Monad public
+  using () renaming (module Instances to MonadInstances)
+open import Haskell.Prim.MonadPlus public
+  using () renaming (module Instances to MonadPlusInstances)
+open import Haskell.Prim.Foldable public
+  renaming (module Instances to FoldableInstances)
+
+
+foldrM : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (a → b → m b) → b → t a → m b
+foldrM f z0 xs = foldl (λ k x z → f x z >>= k) return xs z0
+
+foldlM : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (b → a → m b) → b → t a → m b
+foldlM f z0 xs = foldr (λ x k z → f z x >>= k) return xs z0
+
+traverse₋ : ⦃ Foldable t ⦄ → ⦃ Applicative f ⦄ → (a → f b) → t a → f ⊤
+traverse₋ f = foldr (λ x m → f x *> m) (pure tt)
+
+for₋ : ⦃ Foldable t ⦄ → ⦃ Applicative f ⦄ → t a → (a → f b) → f ⊤
+for₋ = flip traverse₋
+
+mapM₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (a → m b) → t a → m ⊤
+mapM₋ f = foldr (λ x m → f x >> m) (pure tt)
+
+forM₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → t a → (a → m b) → m ⊤
+forM₋ = flip mapM₋
+
+sequenceA₋ : ⦃ Foldable t ⦄ → ⦃ Applicative f ⦄ → t (f a) → f ⊤
+sequenceA₋ = foldr (λ mx my → mx *> my) (pure tt)
+
+sequence₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → t (m a) → m ⊤
+sequence₋ = foldr (λ mx my → mx >> my) (pure tt)
+
+asum : ⦃ Foldable t ⦄ → ⦃ Alternative f ⦄ → t (f a) → f a
+asum = foldr _<|>_ empty
+
+msum : ⦃ Foldable t ⦄ → ⦃ MonadPlus m ⦄ → t (m a) → m a
+msum = asum
+
+concat : ⦃ Foldable t ⦄ → t (List a) → List a
+concat = fold
+
+concatMap : ⦃ Foldable t ⦄ → (a → List b) → t a → List b
+concatMap = foldMap
+
+any : ⦃ Foldable t ⦄ → (a → Bool) → t a → Bool
+any ⦃ i ⦄ = foldMap ⦃ i ⦄ ⦃ MonoidDisj ⦄
+
+all : ⦃ Foldable t ⦄ → (a → Bool) → t a → Bool
+all ⦃ i ⦄ = foldMap ⦃ i ⦄ ⦃ MonoidConj ⦄
+
+and : ⦃ Foldable t ⦄ → t Bool → Bool
+and = all id
+
+or : ⦃ Foldable t ⦄ → t Bool → Bool
+or = any id
+
+maximumBy : ⦃ _ : Foldable t ⦄ → (a → a → Ordering) → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a
+maximumBy {a = a} cmp = foldr1 max'
+  where
+    max' : a → a → a
+    max' x y with cmp x y
+    ...         | GT = x
+    ...         | _  = y
+
+minimumBy : ⦃ _ : Foldable t ⦄ → (a → a → Ordering) → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a
+minimumBy {a = a} cmp = foldr1 min'
+  where
+    min' : a → a → a
+    min' x y with cmp x y
+    ...         | GT = y
+    ...         | _  = x
+
+notElem : ⦃ Foldable t ⦄ → ⦃ Eq a ⦄ → a → t a → Bool
+notElem x t = not (elem x t)
+
+find : ⦃ Foldable t ⦄ → (a → Bool) → t a → Maybe a
+find ⦃ i ⦄ p = foldMap ⦃ i ⦄ ⦃ MonoidFirst ⦄ (λ x → if p x then Just x else Nothing)

lib/base/Haskell/Data/Functor.agda

@@ -0,0 +1,26 @@
+module Haskell.Data.Functor where
+
+open import Haskell.Prim
+open import Haskell.Prim.Tuple
+
+open import Haskell.Prim.Functor public
+  renaming (module Instances to FunctorInstances)
+
+
+infixl 4 _$>_
+_$>_ : ⦃ Functor f ⦄ → f a → (@0 ⦃ a ⦄ → b) → f b
+_$>_ = flip _<$_
+
+infixl 4 _<$>_
+_<$>_ : ⦃ Functor f ⦄ → (a → b) → f a → f b
+_<$>_ = fmap
+
+infixl 1 _<&>_
+_<&>_ : ⦃ Functor f ⦄ → f a → (a → b) → f b
+m <&> f = fmap f m
+
+unzip : ⦃ Functor f ⦄ → f (a × b) -> (f a × f b)
+unzip xs = fst <$> xs , snd <$> xs
+
+void : ⦃ Functor f ⦄ → f a → f ⊤
+void = tt <$_