0 | module Data.Container.Base.Extension.Instances
  1 |
  2 | import Data.DPair
  3 | import Data.Vect
  4 |
  5 | import Data.Container.Base.Object.Definition
  6 | import Data.Container.Base.Extension.Definition
  7 | import Data.Container.Base.Properties.Definitions
  8 |
  9 | import Data.Container.Base.Object.Instances
 10 |
 11 | -- import Data.Functor.Naperian
 12 | import Misc
 13 |
 14 | %hide Prelude.(<|)
 15 |
 16 | namespace ExtensionsOfMainExamples
 17 |   ||| Isomorphic to the Identity
 18 |   public export
 19 |   Scalar' : Type -> Type
 20 |   Scalar' = Ext Scalar
 21 |
 22 |   ||| Isomorphic to Pair
 23 |   public export
 24 |   Pair' : Type -> Type
 25 |   Pair' = Ext Pair
 26 |   
 27 |   ||| Isomorphic to Either
 28 |   public export
 29 |   Either' : Type -> Type
 30 |   Either' = Ext Either
 31 |
 32 |   ||| Isomorphic to Maybe
 33 |   public export
 34 |   Maybe' : Type -> Type
 35 |   Maybe' = Ext Maybe
 36 |   
 37 |   ||| Isomorphic to List
 38 |   public export
 39 |   List' : Type -> Type
 40 |   List' = Ext List
 41 |
 42 |   ||| Isomorphic to Vect
 43 |   public export
 44 |   Vect' : (n : Nat) -> Type -> Type
 45 |   Vect' n = Ext (Vect n)
 46 |
 47 |   ||| Isomorphic to Stream
 48 |   public export
 49 |   Stream' : Type -> Type
 50 |   Stream' = Ext Stream
 51 |
 52 |   ||| Isomorphic to Data.Tree.BinTreeSame
 53 |   public export
 54 |   BinTree' : Type -> Type
 55 |   BinTree' = Ext BinTree
 56 |
 57 |   ||| Isomorphic to Data.Tree.BinTreeNode
 58 |   public export
 59 |   BinTreeNode' : Type -> Type
 60 |   BinTreeNode' = Ext BinTreeNode
 61 |   
 62 |   ||| Isomorphic to Data.Tree.BinTreeLeaf
 63 |   public export
 64 |   BinTreeLeaf' : Type -> Type
 65 |   BinTreeLeaf' = Ext BinTreeLeaf
 66 |
 67 |   {-
 68 |   Technically it is possible to a) use the alias that is below, and b) define Tensor' here, but a decision was made not to do any of these.
 69 |   Rather, Tensor' was defined as a record, and this was done in Data.Tensor as
 70 |   in most linear algebra operations explicit and cumbersome shape annotations 
 71 |   would have been otherwise necessary. Likewise, the definition of usual 
 72 |   interfaces the datatype Tensor' are often involved, making it much simpler
 73 |   to create a separate file for it.
 74 |   -}
 75 |   -- public export
 76 |   -- Tensor' : List Cont -> Type -> Type
 77 |   -- Tensor' cs = Ext (Tensor cs)
 78 |
 79 | public export
 80 | composeExtensions : List Cont -> Type -> Type
 81 | composeExtensions = foldr (\c, f => (Ext c) . f) (Ext Scalar)
 82 |
 83 | namespace ComposeExtensionsVect
 84 |   public export
 85 |   composeExtensions : Vect n Cont -> Type -> Type
 86 |   composeExtensions = foldr @{straightforward} (\c, f => (Ext c) . f) (Ext Scalar)
 87 |
 88 | public export
 89 | [fe] {shape : List Cont} -> Functor (composeExtensions shape) where
 90 |   map {shape = []} f = map f
 91 |   map {shape = (s :: ss)} f = (map @{fe} f <$>)
 92 |
 93 | public export
 94 | EmptyExt : {0 c : Cont} -> IsNaperian c => Ext c Unit
 95 | EmptyExt @{MkIsNaperian _} = () <| \_ => ()
 96 |
 97 | public export
 98 | liftA2ConstCont : IsNaperian c => Ext c a -> Ext c b -> Ext c (a, b)
 99 | liftA2ConstCont @{MkIsNaperian _} ea eb = () <| (\x => (index ea x, index eb x))
100 |
101 | ||| The extension of any Naperian container is an applicative functor
102 | ||| Examples: Scalar, Pair, Vect n, Stream
103 | ||| But not all Applicatives are Naperian, examples being: List and Maybe
104 | public export
105 | IsNaperian c => Applicative (Ext c) where
106 |   pure @{MkIsNaperian _} a = () <| \_ => a
107 |   (<*>) fs xs @{MkIsNaperian _} = uncurry ($) <$> liftA2ConstCont fs xs 
108 |
109 | ||| Generalisation of 'positions' from Data.Functor.Naperian
110 | ||| Works for an arbitrary container, as long as we supply its shape
111 | ||| The definition in Data.Functor.Naperian.positions is for Naperian containers
112 | ||| i.e. containers with a unit shape
113 | public export
114 | positionsCont : {0 c : Cont} -> {sh : c.Shp} -> Ext c (c.Pos sh)
115 | positionsCont = sh <| id
116 |
117 |
118 | ||| The `index` field of an extension defines a "getter" for a container
119 | ||| This is the container setter
120 | public export
121 | set : {0 c : Cont} -> InterfaceOnPositions c Eq =>
122 |   (e : Ext c x) -> c.Pos (shapeExt e) -> x -> Ext c x
123 | set {c=(s !> p)} @{MkI _} (sh <| contentAt) i x
124 |   = sh <| updateAt contentAt (i, x)
125 |