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