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