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