
   0 | module Data.CT.Functor.Instances
   1 | 
   2 | import Data.CT.Category.Definition
   3 | import Data.CT.Category.Instances
   4 | import Data.CT.Functor.Definition
   5 | 
   6 | import Data.Container.Base
   7 | import Data.Container.Additive
   8 | 
   9 | public export
  10 | id : Functor c c
  11 | id = MkFunctor id id
  12 | 
  13 | ||| Functor Type -> Cat^op
  14 | public export
  15 | IndCat : (c : Cat) -> Type
  16 | IndCat c = Functor c (opCat Cat)
  17 | 
  18 | public export
  19 | Const : {c : Cat} -> IndCat c
  20 | Const = MkFunctor (\_ => c) (\_ => id)
  21 | 
  22 | namespace Fam
  23 |   public export
  24 |   FamObj : {c : Cat} -> (a : Type) -> Cat
  25 |   FamObj a = MkCat (a -> c.Obj) (\a', b' => (x : a) -> c.Hom (a' x) (b' x))
  26 | 
  27 |   public export
  28 |   FamMor : {c : Cat} ->
  29 |     {x, y : Type} -> (x -> y) -> Functor (FamObj {c=c} y) (FamObj {c=c} x)
  30 |   FamMor f = MkFunctor (. f) (\j, xx => j (f xx))
  31 | 
  32 |   ||| Functor Type -> Cat^op, we will mostly instantiate this for `c=TypeCat`
  33 |   public export
  34 |   FamIndCat : {c : Cat} -> IndCat TypeCat
  35 |   FamIndCat = MkFunctor (\a => FamObj {c=c} a) FamMor
  36 | 
  37 | ||| Functor which projects the forward part of a dependent lens
  38 | public export
  39 | Base : Functor DLens TypeCat
  40 | Base = MkFunctor Shp (.fwd)
  41 | 
  42 | ||| DLens -> Type -> Cat^op
  43 | public export
  44 | FamDLens : {c : Cat} -> IndCat DLens
  45 | FamDLens = composeFunctors Base (FamIndCat {c=c})
  46 | 
  47 | ||| Functor which projects out the forward part of an additive dependent lens
  48 | public export
  49 | AddBase : Functor AddDLens TypeCat
  50 | AddBase = MkFunctor (.Shp) (.fwd)
  51 | 
  52 | public export
  53 | FamAddDLens : {c : Cat} -> IndCat AddDLens
  54 | FamAddDLens = composeFunctors AddBase (FamIndCat {c=c})
  55 | 
  56 | -- need to check everything from here onwards
  57 | --------------------------------------------------------------------------------
  58 | -- Dependent Types in Poly (Category of Containers & Dependent Lenses)
  59 | --
  60 | -- Reference: von Glehn, "Polynomials and Models of Type Theory", Section 4.1
  61 | --
  62 | -- Key insight: Poly is NOT locally cartesian closed, but:
  63 | --   1. Dependent sums (Σ-types) always exist
  64 | --   2. Dependent products (Π-types) exist only along cartesian morphisms
  65 | --------------------------------------------------------------------------------
  66 | 
  67 | --------------------------------------------------------------------------------
  68 | -- IN TYPE
  69 | --
  70 | -- A type family over `a` is: `a -> Type`
  71 | -- The dependent pair is:     `(x : a ** fam x)`
  72 | -- The dependent function is: `(x : a) -> fam x`
  73 | --------------------------------------------------------------------------------
  74 | 
  75 | namespace Type
  76 |   public export
  77 |   IndexedType : Type -> Type
  78 |   IndexedType a = a -> Type
  79 |   
  80 |   public export
  81 |   TypeDPair : {a : Type} -> IndexedType a -> Type
  82 |   TypeDPair fam = (x : a ** fam x)
  83 | 
  84 |   public export
  85 |   TypeDFun : {a : Type} -> IndexedType a -> Type
  86 |   TypeDFun fam = (x : a) -> fam x
  87 | 
  88 | namespace Cont
  89 |   ||| TODO probably name clash with other "Indexed container"
  90 |   public export
  91 |   IndexedCont : Cont -> Type
  92 |   IndexedCont c = c.Shp -> Cont
  93 |   
  94 |   public export
  95 |   ContDPair : {a : Cont} -> IndexedCont a -> Cont
  96 |   ContDPair a' = ((x ** t) : DPair a.Shp (Shp . a')) !> (a' x).Pos t
  97 | 
  98 |   public export
  99 |   ContProbDPair : {a : Cont} -> IndexedCont a -> Cont
 100 |   ContProbDPair a' = (((x, d) ** t) : DPair (a.Shp, Double) (Shp . a' . fst)) !>
 101 |     (a' x).Pos t
 102 | 
 103 | namespace AddCont
 104 |   public export
 105 |   IndexedAddCont : AddCont -> Type
 106 |   IndexedAddCont c = c.Shp -> AddCont
 107 | 
 108 |   public export
 109 |   AddContDPair : {a : AddCont} -> IndexedAddCont a -> AddCont
 110 |   AddContDPair a' = MkAddCont
 111 |     (((x ** t) : DPair a.Shp ((.Shp) . a')) !> (a' x).Pos t)
 112 |     {mon=(?MonDPairAddCont)}
 113 | 
 114 | 
 115 |   public export
 116 |   AddContDFunFinite : {n : Nat} -> (Fin n -> AddCont) -> AddCont
 117 |   AddContDFunFinite {n = 0} i = Scalar
 118 |   AddContDFunFinite {n = (S k)} i = i 0 >< AddContDFunFinite (i . FS)
 119 | 
 120 |   public export
 121 |   indexShp : {n : Nat} -> {i : Fin n -> AddCont} ->
 122 |     (j : Fin n) ->
 123 |     (AddContDFunFinite i).Shp -> (i j).Shp
 124 |   indexShp {n = (S k)} FZ (s, _) = s
 125 |   indexShp {n = (S k)} {i} (FS y) (_, ss) = indexShp {i=i . FS} y ss
 126 | 
 127 |   public export
 128 |   AddContDFunction : {a : AddCont} -> IndexedAddCont a -> AddCont
 129 |   AddContDFunction a' = MkAddCont 
 130 |     ((s : (x : a.Shp) -> (a' x).Shp) !> ((x : a.Shp) -> (a' x).Pos (s x)))
 131 |     {mon=(?MonDFunctionAddCont)}
 132 |     --{mon=(MkI @{\s => MkComMonoid
 133 |     --  (\l, r => \x => (a' x).Plus (s x) (l x) (r x))
 134 |     --  (\x => (a' x).Zero (s x))})}
 135 | 
 136 | -- public export
 137 | -- ContDPair : (c : Cont) -> IndexedCont c -> Cont
 138 | -- ContDPair c fam = 
 139 | --   (st : (s : c.Shp ** (fam s).Shp)) !> 
 140 | --   Either (c.Pos (fst st)) ((fam (fst st)).Pos (snd st))
 141 | 
 142 | -- Simpler version: just the family positions (no base positions)
 143 | -- This corresponds to the "total space" of a display map
 144 | public export
 145 | ContDPairSimple : (c : Cont) -> IndexedCont c -> Cont
 146 | ContDPairSimple c fam = 
 147 |   (st : (s : c.Shp ** (fam s).Shp)) !> 
 148 |   (fam (fst st)).Pos (snd st)
 149 | 
 150 | --------------------------------------------------------------------------------
 151 | -- DEPENDENT PRODUCT in Poly (Π-types) — MORE SUBTLE
 152 | --
 153 | -- Π-types do NOT always exist in Poly. When they do exist:
 154 | --   - Shapes: Π(s : S). (fam s).Shp     -- sections of the family
 155 | --   - Positions: Σ(s : S). Σ(p : P s). (fam s).Pos (f s)
 156 | --
 157 | -- This only type-checks when S is "small enough" that we can form Π over it.
 158 | --------------------------------------------------------------------------------
 159 | 
 160 | public export
 161 | ContDFun : (c : Cont) -> IndexedCont c -> Cont
 162 | ContDFun c fam = 
 163 |   (f : ((s : c.Shp) -> (fam s).Shp)) !> 
 164 |   (s : c.Shp ** (p : c.Pos s ** (fam s).Pos (f s)))
 165 | 
 166 | --------------------------------------------------------------------------------
 167 | -- EXAMPLES
 168 | --------------------------------------------------------------------------------
 169 | 
 170 | -- Constant family: assigns the same container to every shape
 171 | public export
 172 | constFam : {c : Cont} -> Cont -> IndexedCont c
 173 | constFam d = \_ => d
 174 | 
 175 | -- Trivial family: assigns the unit container (one shape, no positions) to every shape
 176 | public export
 177 | trivialFam : {c : Cont} -> IndexedCont c
 178 | trivialFam = \_ => ((_ : ()) !> Void)
 179 | 
 180 | -- Family that assigns Bool shapes with no positions
 181 | public export
 182 | boolFam : {c : Cont} -> IndexedCont c
 183 | boolFam = \_ => ((_ : Bool) !> Void)