0 | module Data.Container.Base.Object.Instances
  1 |
  2 | import Data.Fin
  3 | import Data.List.Quantifiers
  4 |
  5 | import Data.Container.Base.Object.Definition
  6 | import Data.Container.Base.Product.Definition
  7 | import Data.Container.Base.TreeUtils
  8 |
  9 | import Misc
 10 |
 11 |
 12 | {-------------------------------------------------------------------------------
 13 | Defines basic containers.
 14 | Some of them are possible to express in terms of each other, but we opt to define most of them directly
 15 | -------------------------------------------------------------------------------}
 16 |
 17 | ||| Constant (non-dependent) container: positions do not depend on shapes
 18 | ||| As a polynomial functor: F(X) = aX^b
 19 | public export
 20 | Const2 : Type -> Type -> Cont
 21 | Const2 a b = (_ : a) !> b
 22 |
 23 | ||| Constant container whose shapes and positions coincide
 24 | ||| As a polynomial functor: F(X) = aX^a
 25 | public export 
 26 | Const : Type -> Cont
 27 | Const a = Const2 a a
 28 |
 29 | ||| Naperian container: a constant container with a single shape
 30 | ||| As a polynomial functor: F(X) = X^b
 31 | public export
 32 | Nap : Type -> Cont
 33 | Nap b = Const2 Unit b
 34 |
 35 | ||| Flat container: a constant container with a single position
 36 | ||| As a polynomial functor: F(X) = aX
 37 | public export
 38 | Flat : Type -> Cont
 39 | Flat a = Const2 a Unit
 40 |
 41 | ||| Sharp container: a constant container without any positions
 42 | ||| As a polynomial functor: F(X) = a
 43 | public export
 44 | Sharp : Type -> Cont
 45 | Sharp a = Const2 a Void
 46 |
 47 | ||| Turn a container into a Naperian one by fixing a specific shape
 48 | public export
 49 | At : (c : Cont) -> c.Shp -> Cont
 50 | At c s = Nap (c.Pos s)
 51 |
 52 | ||| Empty container, isomorphic to Void
 53 | ||| As a polynomial functor: F(X) = 0
 54 | ||| Initial container
 55 | public export
 56 | Empty : Cont
 57 | Empty = (_ : Void) !> Void
 58 |
 59 | ||| Container of a single thing
 60 | ||| As a polynomial functor: F(X) = X
 61 | ||| Unit of the tensor and composition product
 62 | public export
 63 | Scalar : Cont
 64 | Scalar = (_ : Unit) !> Unit
 65 |
 66 | ||| Container with a single shape, but no positions. Isomorphic to Unit : Type
 67 | ||| As a polynomial functor: F(X) = 1
 68 | ||| Terminal container
 69 | public export
 70 | UnitCont : Cont
 71 | UnitCont = (_ : Unit) !> Void
 72 |
 73 | ||| Product, container of two things
 74 | ||| Isomorphic to Scalar >*< Scalar
 75 | ||| As a polynomial functor: F(X) = X^2
 76 | public export
 77 | Pair : Cont
 78 | Pair = (_ : Unit) !> Bool
 79 |
 80 | ||| Coproduct, container of either one of two things
 81 | ||| Isomorphic to Scalar >+< Scalar
 82 | ||| As a polynomial functor: F(X) = X + X
 83 | public export
 84 | Either : Cont
 85 | Either = (_ : Bool) !> Unit
 86 |
 87 | ||| Container of either one thing, or nothing
 88 | ||| Isomorphic to Scalar >+< UnitCont
 89 | ||| Initial algebra is Nat
 90 | ||| As a polynomial functor: F(X) = 1 + X
 91 | public export
 92 | Maybe : Cont
 93 | Maybe = (b : Bool) !> (if b then Unit else Void)
 94 |
 95 | ||| Container of either two things, or nothing
 96 | ||| Isomorphic to Pair >+< UnitCont
 97 | ||| Initial algebra is BinTreeShape
 98 | ||| As a polynomial functor: F(X) = 1 + X^2
 99 | public export
100 | MaybeTwo : Cont
101 | MaybeTwo = (b : Bool) !> (if b then Fin 2 else Void)
102 |
103 | ||| List, container with an arbitrary number of things
104 | ||| As a polynomial functor: F(X) = 1 + X + X^2 + X^3 + ...
105 | public export
106 | List : Cont
107 | List = (n : Nat) !> Fin n
108 |
109 | ||| Non-empty lists, container with an arbitrary number of things
110 | ||| As a polynomial functor: F(X) = X + X^2 + X^3 + ...
111 | public export
112 | List1 : Cont
113 | List1 = (n : Nat) !> Fin (S n)
114 |
115 |
116 | ||| Bags/multisets, *quotient* containers
117 | ||| As an *analytic* functor: F(X) = 1 + X + X^2 + X^3 + ... / S_n
118 | ||| Not enforcing the quotient at the moment
119 | ||| See also `Data.Bag`
120 | public export
121 | Bag : Cont
122 | Bag = (n : Nat) !> FiniteSet n
123 |
124 | ||| Vect, container of a fixed/known number of things
125 | ||| As a polynomial functor: F(X) = X^n
126 | public export
127 | Vect : List .Shp -> Cont
128 | Vect = At {c=List}
129 |
130 | ||| Grid, container of things arranged along two axes
131 | ||| As a polynomial functor: F(X) = X^(hw)
132 | public export
133 | Grid : (List .Shp, List .Shp) -> Cont
134 | Grid (h, w) = (Vect h) >< (Vect w)
135 |
136 | ||| Container of an infinite number of things
137 | ||| As a polynomial functor: F(X) = X^Nat
138 | public export
139 | Stream : Cont
140 | Stream = (_ : Unit) !> Nat
141 |
142 | ||| Container of things stored at nodes and leaves of a binary tree
143 | ||| As a polynomial functor: F(X) = 1 + 2X + 3X^2 + 7X^3 + ...
144 | public export
145 | BinTree : Cont
146 | BinTree = (b : BinTreeShape) !> BinTreePos b
147 |
148 | ||| Container of things stored at nodes of a binary tree
149 | ||| As a polynomial functor: F(X) = 1 + X + 2X^2 + 5X^3 +
150 | public export
151 | BinTreeNode : Cont
152 | BinTreeNode = (b : BinTreeShape) !> BinTreePosNode b
153 |
154 | ||| Container of things stored at leaves of a binary tree
155 | ||| As a polynomial functor: F(X) = X + X^2 + 2X^3 + 5X^4 +
156 | public export
157 | BinTreeLeaf : Cont
158 | BinTreeLeaf = (b : BinTreeShape) !> BinTreePosLeaf b
159 |
160 | ||| Tensors are containers
161 | ||| As a polynomial functor: F(X) = ?
162 | public export
163 | Tensor : List Cont -> Cont
164 | Tensor = foldr (>@) Scalar
165 |
166 | public export
167 | CartesianTensor : List Cont -> Cont
168 | CartesianTensor = foldr (>*<) UnitCont
169 |
170 | public export
171 | HancockTensor : List Cont -> Cont
172 | HancockTensor = foldr (><) Scalar
173 |
174 | public export
175 | CoproductTensor : List Cont -> Cont
176 | CoproductTensor = foldr (>+<) Empty
177 |
178 | ||| Ignoring universe levels here
179 | ||| This should be the analogue of `Type : Type`
180 | public export
181 | ContUniverse : Cont
182 | ContUniverse = (_ : (s : Type ** s -> Type)) !> Void