0 | module Data.Functor.Naperian
  1 |
  2 | import Data.Vect
  3 |
  4 | %hide Data.Vect.transpose
  5 |
  6 | -- todo this isn't necessary anymore?
  7 | -- Needed to define transposition, and diagonal elements
  8 | {-
  9 | Lists -> not Naperian! Their shape isn't uniform (they can be of different lengths)
 10 | Stream -> Naperian, and is represented by Nat
 11 | Vect n ->Naperian, and are represented by Fin n
 12 |
 13 | BinTree in general is not Naperian, but if we restrict to trees of a particular shape, then they are Naperian
 14 |
 15 | Naperian functors arise out of containers with a unit shape
 16 | * Would ragged shapes imply dependent types?
 17 | -}
 18 |
 19 | public export
 20 | interface Applicative f => Naperian f where
 21 |     Log : Type -- perhaps a better name is Shape
 22 |     lookup : f a -> (Log -> a) -- This and the line below
 23 |     tabulate : (Log -> a) -> f a -- are an isomorphism
 24 |
 25 | public export
 26 | positions : Naperian f => f (Log {f=f})
 27 | positions = tabulate id
 28 |
 29 | public export
 30 | transpose : Naperian f => Naperian g => f (g a) -> g (f a)
 31 | transpose x = tabulate <$> tabulate (flip (lookup . (lookup x)))
 32 |
 33 | public export
 34 | {n : Nat} -> Naperian (Vect n) where
 35 |     Log = Fin n
 36 |     lookup = flip index
 37 |     tabulate = Vect.Fin.tabulate
 38 |
 39 | public export
 40 | Naperian f => Naperian g => Naperian (g . f) using Applicative.Compose where
 41 |   Log = (Log {f=f}, Log {f=g})
 42 |   lookup gfa (pf, pg) = lookup (lookup gfa pg) pf
 43 |   tabulate f = tabulate <$> tabulate (flip (curry f))
 44 |
 45 |
 46 | vectPositionsEx : Vect 3 (Fin 3)
 47 | vectPositionsEx = positions
 48 |
 49 | -- reshapeTensorANap : {shape : Vect n Nat} -> {newShape : Vect m Nat}
 50 | --   -> TensorA shape a
 51 | --   -> (newShape : Vect n Nat)
 52 | --   -> {auto prf : prod shape = prod newShape}
 53 | --   -> TensorA newShape a
 54 | -- reshapeTensorANap t newShape = let tR = lookup t in tabulate ?aa
 55 | -- 
 56 | -- reshapeIndex : {shape : Vect n Nat} -> {newShape : Vect m Nat}
 57 | --   -> {auto prf : prod shape = prod newShape}
 58 | --   -> IndexT newShape
 59 | --   -> IndexT shape
 60 | -- reshapeIndex [] = ?reshapeIndex_rhs_0
 61 | -- reshapeIndex (x :: xs) = ?reshapeIndex_rhs_1
 62 |
 63 |
 64 | -- mapNats : {t, t' : Vect n Nat} -> {auto prf : prod t = prod t'}
 65 | --   -> Fin (prod t) -> Fin (prod t')
 66 | -- mapNats i = ?mapNats_rhs
 67 |
 68 |
 69 | -- reshapeIndex' : IndexT [2, 3]
 70 | --   -> IndexT [6]
 71 | -- reshapeIndex' (i :: j :: Nil) = ?yuu :: Nil
 72 |
 73 | -- tensorPositionsEx : TensorA [3, 3, 3] (IndexT [3, 3, 3])
 74 | -- tensorPositionsEx = positions
 75 |
 76 |   -- not sure how to represent Pair, it's curried?
 77 | -- Naperian (Pair) where
 78 | --     Log = Bool
 79 | --     lookup = pairLookup
 80 | --     tabulate f = (f False, f True)
 81 |     
 82 |
 83 |
 84 | {-
 85 |            a
 86 |          x  y
 87 |
 88 |   a'                a''
 89 | x' y'             x'' y''
 90 |
 91 | transposed would be
 92 |
 93 |
 94 |            a
 95 |          a'  a''
 96 |
 97 |   x                  y
 98 | x' x''             y' y''
 99 |
100 | ---
101 |
102 | If it was ragged we would not be able to transpose it
103 | -}
104 |