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.Extension.Definition
 9 | import Data.Container.Additive.Product.Definition
10 | import Data.Container.Additive.Properties.Definition
11 |
12 | ||| Constant (non-dependent) add. container, positions not dependent on shapes
13 | ||| As a polynomial functor: F(Y) = aY^b
14 | public export
15 | Const2 : Type -> ComMonoid -> AddCont
16 | Const2 a m = MkAddCont a (\_ => m)
17 |
18 | namespace NumConst
19 |   ||| Constant additive container whose shapes and positions coincide
20 |   ||| Also arises from Num instance
21 |   public export
22 |   Const : (a : Type) -> (mon : ComMonoid a) => AddCont
23 |   Const a = Const2 a (a ** mon)
24 |
25 | namespace Const
26 |   public export
27 |   data IsConst : AddCont -> Type where
28 |     MkIsConst : (p : Type) -> (mon : ComMonoid p) => IsConst (Const p)
29 |
30 | ||| Every constant additive container on a numeric type carries `Num` on its
31 | ||| positions: `(Const p @{mon}).PosSet s` reduces to `p` at every shape, so the
32 | ||| witness is the numeric instance itself, constantly.
33 | ||| A `%hint`, so that matching an `IsConst` witness into scope is enough for
34 | ||| search to discharge an `InterfaceOnPositions` goal.
35 | %hint
36 | public export
37 | numOnPositions : {0 p : Type} -> (num : Num p) => (mon : ComMonoid p) =>
38 |   InterfaceOnPositions (Const p @{mon}) Num
39 | numOnPositions = MkI (\_ => num)
40 |
41 | ||| Naperian additive container: a constant container with a single shape
42 | ||| As a polynomial functor: F(Y) = Y^b
43 | public export
44 | Nap : ComMonoid -> AddCont
45 | Nap b = Const2 Unit b
46 |
47 | ||| Flat additive container: a constant container with a single position
48 | ||| As a polynomial functor: F(Y) = aY
49 | ||| Notably, unlike with `Data.Container.Base`, there is no `Sharp`
50 | public export
51 | Flat : Type -> AddCont
52 | Flat a = Const2 a (Unit ** %search)
53 |
54 |
55 | ||| Empty additive container
56 | ||| As a polynomial functor: F(Y) = 0
57 | ||| Initial additive container
58 | public export
59 | Empty : AddCont
60 | Empty = MkAddCont Void absurd
61 |
62 |
63 | ||| Container of a single thing
64 | ||| As a polynomial functor: F(Y) = U(Y) where U is forgetful functor
65 | ||| Unit of the tensor product
66 | public export
67 | Scalar : AddCont
68 | Scalar = Nap (Nat ** %search)
69 |
70 |
71 | ||| Additive container with a single shape and position
72 | ||| As a polynomial functor F(Y) = 1
73 | ||| Terminal additive container
74 | public export
75 | UnitCont : AddCont
76 | UnitCont = Const Unit