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 | ||| Empty container, isomorphic to Void
 11 | ||| As a polynomial functor: F(X) = 0
 12 | ||| Initial container
 13 | public export
 14 | Empty : Cont
 15 | Empty = (_ : Void) !> Void
 16 |
 17 | ||| Container of a single thing
 18 | ||| As a polynomial functor: F(X) = X
 19 | public export
 20 | Scalar : Cont
 21 | Scalar = (_ : Unit) !> Unit
 22 |
 23 | ||| Container with a single shape, but no positions. Isomorphic to Unit : Type
 24 | ||| As a polynomial functor: F(X) = 1
 25 | ||| Terminal container
 26 | public export
 27 | UnitCont : Cont
 28 | UnitCont = (_ : Unit) !> Void
 29 |
 30 | ||| Product, container of two things
 31 | ||| Isomorphic to Scalar >*< Scalar
 32 | ||| As a polynomial functor: F(X) = X^2
 33 | public export
 34 | Pair : Cont
 35 | Pair = (_ : Unit) !> Bool
 36 |
 37 | ||| Coproduct, container of either one of two things
 38 | ||| Isomorphic to Scalar >+< Scalar
 39 | ||| As a polynomial functor: F(X) = X + X
 40 | public export
 41 | Either : Cont
 42 | Either = (_ : Bool) !> Unit
 43 |
 44 | ||| Container of either one thing, or nothing
 45 | ||| Isomorphic to Scalar >+< UnitCont
 46 | ||| Initial algebra is Nat
 47 | ||| As a polynomial functor: F(X) = 1 + X
 48 | public export
 49 | Maybe : Cont
 50 | Maybe = (b : Bool) !> (if b then Unit else Void)
 51 |
 52 | ||| Container of either two things, or nothing
 53 | ||| Isomorphic to Pair >+< UnitCont
 54 | ||| Initial algebra is BinTreeShape
 55 | ||| As a polynomial functor: F(X) = 1 + X^2
 56 | public export
 57 | MaybeTwo : Cont
 58 | MaybeTwo = (b : Bool) !> (if b then Fin 2 else Void)
 59 |
 60 | ||| List, container with an arbitrary number of things
 61 | ||| As a polynomial functor: F(X) = 1 + X + X^2 + X^3 + ...
 62 | public export
 63 | List : Cont
 64 | List = (n : Nat) !> Fin n
 65 |
 66 | ||| Vect, container of a fixed/known number of things
 67 | ||| As a polynomial functor: F(X) = X^n
 68 | public export
 69 | Vect : List .Shp -> Cont
 70 | Vect n = (_ : Unit) !> Fin n
 71 |
 72 | ||| Container of an infinite number of things
 73 | ||| As a polynomial functor: F(X) = X^Nat
 74 | public export
 75 | Stream : Cont
 76 | Stream = (_ : Unit) !> Nat
 77 |
 78 | ||| Container of things stored at nodes and leaves of a binary tree
 79 | ||| As a polynomial functor: F(X) = 1 + 2X + 3X^2 + 7X^3 + ...
 80 | public export
 81 | BinTree : Cont
 82 | BinTree = (b : BinTreeShape) !> BinTreePos b
 83 |
 84 | ||| Container of things stored at nodes of a binary tree
 85 | ||| As a polynomial functor: F(X) = 1 + X + 2X^2 + 5X^3 +
 86 | public export
 87 | BinTreeNode : Cont
 88 | BinTreeNode = (b : BinTreeShape) !> BinTreePosNode b
 89 |
 90 | ||| Container of things stored at leaves of a binary tree
 91 | ||| As a polynomial functor: F(X) = X + X^2 + 2X^3 + 5X^4 +
 92 | public export
 93 | BinTreeLeaf : Cont
 94 | BinTreeLeaf = (b : BinTreeShape) !> BinTreePosLeaf b
 95 |
 96 | ||| Tensors are containers
 97 | ||| As a polynomial functor: F(X) = ?
 98 | public export
 99 | Tensor : List Cont -> Cont
100 | Tensor = foldr (>@) Scalar
101 |
102 | public export
103 | CartesianTensor : List Cont -> Cont
104 | CartesianTensor = foldr (>*<) UnitCont
105 |
106 | public export
107 | HancockTensor : List Cont -> Cont
108 | HancockTensor = foldr (><) Scalar
109 |
110 | public export
111 | CoproductTensor : List Cont -> Cont
112 | CoproductTensor = foldr (>+<) Empty
113 |
114 |
115 | ||| Can't believe this works?
116 | public export
117 | Sample : Nat -> Cont
118 | Sample n = Const2 (Dist n) (Fin n)
119 |