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