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 | public export
31 | (++) : Bag a -> Bag a -> Bag a
32 | (MkBag xs) ++ (MkBag ys) = MkBag (xs ++ ys)
33 |
34 | public export
35 | Functor Bag where
36 |   map f (MkBag xs) = MkBag (map f xs)
37 |
38 | public export
39 | Applicative Bag where
40 |   pure a = MkBag (pure a)
41 |   (MkBag fs) <*> (MkBag xs) = MkBag (fs <*> xs)
42 |
43 | public export
44 | Monad Bag where
45 |   join (MkBag b) = MkBag $ join (toList <$> b)
46 |
47 | public export
48 | Foldable Bag where
49 |   foldr f z (MkBag xs) = foldr f z xs
50 |
51 |
52 | namespace Quantifiers
53 |   -- biproduct, because bag is finite
54 |   public export
55 |   All : (p : a -> Type) -> Bag a -> Type
56 |   All p (MkBag xs) = All p xs
57 |
58 |   public export
59 |   Any : (p : a -> Type) -> Bag a -> Type
60 |   Any p (MkBag xs) = Any p xs
61 |     
62 |
63 |
64 | -- The input always comes with the data of a position, by virtue of needing to be stored on the disk?