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