0 | module Data.Container.Additive.Object.Instances
 1 |
 2 | import Data.List.Quantifiers
 3 | import Data.Vect.Quantifiers
 4 |
 5 | import Data.Container.Base
 6 | import Data.ComMonoid
 7 | import public Data.Container.Additive.Object.Definition
 8 | import Data.Container.Additive.Product.Definition
 9 |
10 | ||| Constant (non-dependent) add. container, positions not dependent on shapes
11 | ||| As a polynomial functor: F(Y) = aY^b
12 | public export
13 | Const2 : Type -> ComMonoid -> AddCont
14 | Const2 a m = MkAddCont a (\_ => m)
15 |
16 | namespace NumConst
17 |   ||| Constant additive container whose shapes and positions coincide
18 |   ||| Also arises from Num instance
19 |   public export
20 |   Const : (a : Type) -> (mon : ComMonoid a) => AddCont
21 |   Const a = Const2 a (a ** mon)
22 |
23 | ||| Naperian additive container: a constant container with a single shape
24 | ||| As a polynomial functor: F(Y) = Y^b
25 | public export
26 | Nap : ComMonoid -> AddCont
27 | Nap b = Const2 Unit b
28 |
29 | ||| Flat additive container: a constant container with a single position
30 | ||| As a polynomial functor: F(Y) = aY
31 | ||| Notably, unlike with `Data.Container.Base`, there is no `Sharp`
32 | public export
33 | Flat : Type -> AddCont
34 | Flat a = Const2 a (Unit ** %search)
35 |
36 | ||| Empty additive container
37 | ||| As a polynomial functor: F(Y) = 0
38 | ||| Initial additive container
39 | public export
40 | Empty : AddCont
41 | Empty = MkAddCont Void absurd
42 |
43 | ||| Container of a single thing
44 | ||| As a polynomial functor: F(Y) = U(Y) where U is forgetful functor
45 | ||| Unit of the tensor product
46 | public export
47 | Scalar : AddCont
48 | Scalar = Nap (Nat ** %search)
49 |
50 | ||| Additive container with a single shape and position
51 | ||| As a polynomial functor F(Y) = 1
52 | ||| Terminal additive container
53 | public export
54 | UnitCont : AddCont
55 | UnitCont = Const Unit
56 |
57 | public export
58 | Maybe : AddCont -> AddCont
59 | Maybe c = UnitCont >+< c
60 |
61 |