0 | module Data.SOP.POP
  1 |
  2 | import Data.SOP.Utils
  3 | import Data.SOP.Interfaces
  4 | import Data.SOP.NP
  5 |
  6 | import Decidable.Equality
  7 |
  8 | %default total
  9 |
 10 | ||| A product of products.
 11 | |||
 12 | ||| The elements of the inner products are
 13 | ||| applications of the parameter f. The type POP is indexed by the list of lists
 14 | ||| that determines the lengths of both the outer and all the inner products, as
 15 | ||| well as the types of all the elements of the inner products.
 16 | |||
 17 | ||| A POP is reminiscent of a two-dimensional table (but the inner lists can all be
 18 | ||| of different length). In the context of the SOP approach to
 19 | ||| generic programming, a POP is useful to represent information
 20 | ||| that is available for all arguments of all constructors of a datatype.
 21 | public export
 22 | data POP_ : (k : Type) -> (f : k -> Type) -> (kss : List (List k)) -> Type where
 23 |   MkPOP : NP_ (List k) (NP_ k f) kss -> POP_ k f kss
 24 |
 25 | ||| Type alias for `POP_` with type parameter `k` being
 26 | ||| implicit. This reflects the kind-polymorphic data type
 27 | ||| in Haskell.
 28 | public export
 29 | POP : {k : Type} -> (f : k -> Type) -> (kss : List (List k)) -> Type
 30 | POP = POP_ k
 31 |
 32 | public export %inline
 33 | unPOP : POP_ k f kss -> NP_ (List k) (NP_ k f) kss
 34 | unPOP (MkPOP np) = np
 35 |
 36 | --------------------------------------------------------------------------------
 37 | --          Specialized Interface Functions
 38 | --------------------------------------------------------------------------------
 39 |
 40 | ||| Specialiced version of `hmap`
 41 | public export
 42 | mapPOP : (fun : forall a . f a -> g a) -> POP f kss -> POP g kss
 43 | mapPOP fun = MkPOP . mapNP (\p => mapNP fun p) . unPOP
 44 |
 45 | ||| Specialization of `hpure`.
 46 | public export
 47 | purePOP : {kss : _} -> (forall a . f a) -> POP f kss
 48 | purePOP {kss = []}     fun = MkPOP []
 49 | purePOP {kss = _ :: _} fun = let (MkPOP nps) = purePOP fun
 50 |                               in MkPOP $ pureNP fun :: nps
 51 |
 52 | ||| Specialization of `hap`.
 53 | public export
 54 | hapPOP : POP (\a => f a -> g a) kss -> POP f kss -> POP g kss
 55 | hapPOP (MkPOP fs) = MkPOP . hliftA2 (\p => hapNP p) fs . unPOP
 56 |
 57 | ||| Specialization of `hfoldl`
 58 | public export
 59 | foldlPOP : (fun : acc -> el -> acc) -> acc -> POP (K el) kss -> acc
 60 | foldlPOP _   acc (MkPOP [])     = acc
 61 | foldlPOP fun acc (MkPOP (h::t)) = foldlPOP fun (foldlNP fun acc h) (MkPOP t)
 62 |
 63 | ||| Specialization of `hfoldr`
 64 | public export
 65 | foldrPOP : (fun : el -> Lazy acc -> acc) -> Lazy acc -> POP (K el) kss -> acc
 66 | foldrPOP _   acc (MkPOP [])     = acc
 67 | foldrPOP fun acc (MkPOP (h::t)) = foldrNP fun (foldrPOP fun acc (MkPOP t)) h
 68 |
 69 | ||| Specialization of `hsequence`
 70 | public export
 71 | sequencePOP : Applicative g => POP (\a => g (f a)) kss -> g (POP f kss)
 72 | sequencePOP = map MkPOP . sequenceNP . mapNP (\p => sequenceNP p) . unPOP
 73 |
 74 | ||| Specialization of `hcollapse`
 75 | public export
 76 | collapsePOP : POP (K a) kss -> (List $ List a)
 77 | collapsePOP = collapseNP . mapNP (\v => collapseNP v) . unPOP
 78 |
 79 | --------------------------------------------------------------------------------
 80 | --          Interface Conversions
 81 | --------------------------------------------------------------------------------
 82 |
 83 | ||| This is needed to implement `Ord` below.
 84 | public export %hint
 85 | ordToEqPOP :  POP (Ord . f) kss -> POP (Eq . f) kss
 86 | ordToEqPOP = mapPOP (\_ => %search)
 87 |
 88 | ||| This is needed to implement `Monoid` below.
 89 | public export %hint
 90 | monoidToSemigroupPOP : POP (Monoid . f) kss -> POP (Semigroup . f) kss
 91 | monoidToSemigroupPOP = mapPOP (\_ => %search)
 92 |
 93 | ||| Converts a POP of constraints to an n-ary sum
 94 | ||| holding constrains about the inner n-ary sum.
 95 | |||
 96 | ||| Example : POP Eq typess -> NP (Eq . NP I) typess
 97 | |||
 98 | ||| In the example above, we convert a POP of `Eq` instances
 99 | ||| into an n-ary sum of Eq instances of the inner products.
100 | ||| This allows us to for instance implent `Eq (POP f kss) ` below
101 | ||| via a direct call to (==) specialized to Eq (NP (NP f) kss).
102 | public export %hint
103 | popToNP :
104 |      POP_ k (c . f) kss
105 |   -> {auto prf : forall ks . NP_ k (c . f) ks => c (NP_ k f ks)}
106 |   -> NP_ (List k) (c . NP_ k f) kss
107 | popToNP (MkPOP nps) = hmap (\_ => prf) nps
108 |
109 | --------------------------------------------------------------------------------
110 | --          Implementations
111 | --------------------------------------------------------------------------------
112 |
113 | public export %inline
114 | HPure k (List $ List k) (POP_ k) where hpure  = purePOP
115 |
116 | public export %inline
117 | HFunctor k (List $ List k) (POP_ k) where hmap  = mapPOP
118 |
119 | public export %inline
120 | HAp k (List $ List k) (POP_ k) (POP_ k) where hap = hapPOP
121 |
122 | public export %inline
123 | HFold k (List $ List k) (POP_ k) where
124 |   hfoldl = foldlPOP
125 |   hfoldr = foldrPOP
126 |
127 | public export %inline
128 | HSequence k (List $ List k) (POP_ k) where hsequence = sequencePOP
129 |
130 | public export %inline
131 | HCollapse k (List $ List k) (POP_ k) (List . List) where
132 |   hcollapse = collapsePOP
133 |
134 | public export
135 | POP (Eq . f) kss => Eq (POP_ k f kss) where
136 |   MkPOP a == MkPOP b = a == b
137 |
138 | public export
139 | POP (Ord . f) kss => Ord (POP_ k f kss) where
140 |   compare (MkPOP a) (MkPOP b) = compare a b
141 |
142 | public export
143 | POP (Semigroup . f) kss => Semigroup (POP_ k f kss) where
144 |   MkPOP a <+> MkPOP b = MkPOP $ a <+> b
145 |
146 | public export
147 | POP (Monoid . f) kss => Monoid (POP_ k f kss) where
148 |   neutral = MkPOP neutral
149 |
150 | public export
151 | POP (Show . f) kss => Show (POP_ k f kss) where
152 |   showPrec p (MkPOP np) = showCon p "MkPOP" (show np)
153 |
154 | private
155 | mkPOPInjective : MkPOP a = MkPOP b -> a = b
156 | mkPOPInjective Refl = Refl
157 |
158 | public export
159 | POP (DecEq . f) kss => DecEq (POP_ k f kss) where
160 |   decEq (MkPOP a) (MkPOP b) with (decEq a b)
161 |     decEq (MkPOP a) (MkPOP a) | Yes Refl   = Yes $ cong MkPOP Refl
162 |     decEq (MkPOP a) (MkPOP b) | No  contra = No (contra . mkPOPInjective)
163 |