0 | module Data.Bag
 1 |
 2 | import Misc
 3 | import Data.List.Quantifiers
 4 |
 5 | ||| Bag ~ Multiset, a set where each element can appear multiple times
 6 | ||| Free *commutative* monoid on a set
 7 | ||| Equivalently, a list without order, i.e. quotiented out by permutations
 8 | ||| Using the list representation here, without enforcing permutation quotient
 9 | public export
10 | record Bag (a : Type) where
11 |   constructor MkBag
12 |   toList : List a
13 |
14 | public export
15 | Multiset : Type -> Type
16 | Multiset = Bag
17 |
18 | public export
19 | multiplicities : Eq a => List a -> (a -> Nat)
20 | multiplicities [] = const 0
21 | multiplicities (x :: xs) = \y => applyWhen (x == y) (1 +) (multiplicities xs y)
22 |
23 | namespace Bag 
24 |   ||| A multiset is equivalently a function `a -> Nat` with finite support
25 |   public export
26 |   multiplicities : Eq a => Bag a -> (a -> Nat)
27 |   multiplicities = multiplicities . toList
28 |
29 |
30 | export infixr 7 ++
31 |
32 | public export
33 | (++) : Bag a -> Bag a -> Bag a
34 | (MkBag xs) ++ (MkBag ys) = MkBag (xs ++ ys)
35 |
36 | public export
37 | Functor Bag where
38 |   map f (MkBag xs) = MkBag (map f xs)
39 |
40 | public export
41 | Applicative Bag where
42 |   pure a = MkBag (pure a)
43 |   (MkBag fs) <*> (MkBag xs) = MkBag (fs <*> xs)
44 |
45 | public export
46 | Monad Bag where
47 |   join (MkBag b) = MkBag $ join (toList <$> b)
48 |
49 | public export
50 | Foldable Bag where
51 |   foldr f z (MkBag xs) = foldr f z xs
52 |
53 |
54 | namespace Quantifiers
55 |   public export
56 |   All : (p : a -> Type) -> Bag a -> Type
57 |   All p (MkBag xs) = All p xs
58 |
59 |   public export
60 |   Any : (p : a -> Type) -> Bag a -> Type
61 |   Any p (MkBag xs) = Any p xs
62 |     
63 |
64 |
65 | -- The input always comes with the data of a position, by virtue of needing to be stored on the disk?