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