
   0 | module Data.SOP.SOP
   1 | 
   2 | import Data.List.Elem
   3 | 
   4 | import Data.SOP.NP
   5 | import Data.SOP.NS
   6 | import Data.SOP.POP
   7 | import Data.SOP.Utils
   8 | import Data.SOP.Interfaces
   9 | import Data.Maybe
  10 | 
  11 | import Decidable.Equality
  12 | 
  13 | %default total
  14 | 
  15 | ||| A sum of products.
  16 | |||
  17 | ||| The elements of the (inner) products
  18 | ||| are applications of the parameter f. The type SOP_ is indexed by the list of
  19 | ||| lists that determines the sizes of both the (outer) sum and all the (inner)
  20 | ||| products, as well as the types of all the elements of the inner products.
  21 | |||
  22 | ||| A SOP I reflects the structure of a normal Idris datatype. The sum structure
  23 | ||| represents the choice between the different constructors, the product structure
  24 | ||| represents the arguments of each constructor.
  25 | public export
  26 | data SOP_ : (k : Type) -> (f : k -> Type) -> (kss : List $ List k) -> Type where
  27 |   MkSOP : NS_ (List k) (NP_ k f) kss -> SOP_ k f kss
  28 | 
  29 | ||| Type alias for `SOP_` with type parameter `k` being
  30 | ||| implicit. This reflects the kind-polymorphic data type
  31 | ||| in Haskell.
  32 | public export
  33 | SOP : {k : Type} -> (f : k -> Type) -> (kss : List (List k)) -> Type
  34 | SOP = SOP_ k
  35 | 
  36 | public export %inline
  37 | unSOP : SOP_ k f kss -> NS_ (List k) (NP_ k f) kss
  38 | unSOP (MkSOP ns) = ns
  39 | 
  40 | --------------------------------------------------------------------------------
  41 | --          Specialized Interface Functions
  42 | --------------------------------------------------------------------------------
  43 | 
  44 | ||| Specialiced version of `hmap`
  45 | public export
  46 | mapSOP : (fun : forall a . f a -> g a) -> SOP f kss -> SOP g kss
  47 | mapSOP fun = MkSOP . mapNS (\p => mapNP fun p) . unSOP
  48 | 
  49 | ||| Specialization of `hap`
  50 | public export
  51 | hapSOP : POP (\a => f a -> g a) kss -> SOP f kss -> SOP g kss
  52 | hapSOP (MkPOP fs) = MkSOP . hliftA2 (\p => hapNP p) fs . unSOP
  53 | 
  54 | ||| Specialization of `hfoldl`
  55 | public export
  56 | foldlSOP : (fun : acc -> el -> acc) -> acc -> SOP (K el) kss -> acc
  57 | foldlSOP fun acc (MkSOP $ Z vs) = foldlNP fun acc vs
  58 | foldlSOP fun acc (MkSOP $ S x)  = foldlSOP fun acc (MkSOP x)
  59 | 
  60 | ||| Specialization of `hfoldr`
  61 | public export %inline
  62 | foldrSOP : (fun : el -> Lazy acc -> acc) -> Lazy acc -> SOP (K el) kss -> acc
  63 | foldrSOP fun acc (MkSOP $ Z vs) = foldrNP fun acc vs
  64 | foldrSOP fun acc (MkSOP $ S x)  = foldrSOP fun acc (MkSOP x)
  65 | 
  66 | ||| Specialization of `hsequence`
  67 | public export
  68 | sequenceSOP : Applicative g => SOP (\a => g (f a)) kss -> g (SOP f kss)
  69 | sequenceSOP = map MkSOP . sequenceNS . mapNS (\p => sequenceNP p) . unSOP
  70 | 
  71 | ||| Specialization of `hcollapse`
  72 | public export
  73 | collapseSOP : SOP (K a) kss -> List a
  74 | collapseSOP = collapseNS . mapNS (\v => collapseNP v) . unSOP
  75 | 
  76 | --------------------------------------------------------------------------------
  77 | --          Injections
  78 | --------------------------------------------------------------------------------
  79 | 
  80 | ||| An injection into an n-ary sum of products takes an n-ary product of
  81 | ||| the correct type and wraps it in one of the sum's possible choices.
  82 | public export
  83 | 0 InjectionSOP : (f : k -> Type) -> (kss : List $ List k) -> (vs : List k) -> Type
  84 | InjectionSOP f kss vs = NP f vs -> K (SOP f kss) vs
  85 | 
  86 | ||| The set of injections into an n-ary sum `NS f ks` can
  87 | ||| be wrapped in a corresponding n-ary product.
  88 | public export
  89 | injectionsSOP : {kss : _} -> NP_ (List k) (InjectionSOP f kss) kss
  90 | injectionsSOP = hmap (MkSOP .) $ injections {ks = kss}
  91 | 
  92 | ||| Applies all injections to a product of products of values.
  93 | |||
  94 | ||| This is not implemented in terms of `injectionsSOP` for the
  95 | ||| following reason: Since we have access to the structure
  96 | ||| of the product of products and thus `kss`, we do not need a
  97 | ||| runtime reference of `kss`. Therefore, when applying
  98 | ||| injections to a product of products, prefer this function
  99 | ||| over a combination involving `injectionsSOP`.
 100 | public export
 101 | apInjsPOP_ : POP f kss -> NP (K $ SOP f kss) kss
 102 | apInjsPOP_  = mapNP (\ns => MkSOP ns) . apInjsNP_ . unPOP
 103 | 
 104 | ||| Alias for `collapseNP . apInjsPOP_`
 105 | public export
 106 | apInjsPOP : POP f kss -> List (SOP f kss)
 107 | apInjsPOP = collapseNP . apInjsPOP_
 108 | 
 109 | ||| Injects a product into an n-ary sum of products.
 110 | public export
 111 | injectSOP : {0 ks : List k} -> (v : NP f ks) -> {auto prf : Elem ks kss} -> SOP f kss
 112 | injectSOP v = MkSOP $ inject v
 113 | 
 114 | ||| Tries to extract a product of the given type from an
 115 | ||| n-ary sum of products.
 116 | public export
 117 | extractSOP :
 118 |      (0 ks : List k)
 119 |   -> SOP f kss
 120 |   -> {auto prf : Elem ks kss}
 121 |   -> Maybe (NP f ks)
 122 | extractSOP ks (MkSOP ns) = extract ks {prf} ns
 123 | 
 124 | --------------------------------------------------------------------------------
 125 | --          Implementations
 126 | --------------------------------------------------------------------------------
 127 | 
 128 | public export %inline
 129 | HFunctor k (List $ List k) (SOP_ k) where hmap = mapSOP
 130 | 
 131 | public export %inline
 132 | HAp k (List $ List k) (POP_ k) (SOP_ k) where hap = hapSOP
 133 | 
 134 | public export %inline
 135 | HFold k (List $ List k) (SOP_ k) where
 136 |   hfoldl = foldlSOP
 137 |   hfoldr = foldrSOP
 138 | 
 139 | public export
 140 | HSequence k (List $ List k) (SOP_ k) where hsequence = sequenceSOP
 141 | 
 142 | public export %inline
 143 | HCollapse k (List $ List k) (SOP_ k) List where hcollapse = collapseSOP
 144 | 
 145 | public export
 146 | POP (Eq . f) kss => Eq (SOP_ k f kss) where
 147 |   MkSOP a == MkSOP b = a == b
 148 | 
 149 | public export
 150 | POP (Ord . f) kss => Ord (SOP_ k f kss) where
 151 |   compare (MkSOP a) (MkSOP b) = compare a b
 152 | 
 153 | public export
 154 | POP (Show . f) kss => Show (SOP_ k f kss) where
 155 |   showPrec p (MkSOP ns) = showCon p "MkSOP" (showArg ns)
 156 | 
 157 | ||| Sums of products have instances of `Semigroup` and `Monoid`
 158 | ||| only when they consist of a single choice, which must itself be
 159 | ||| a `Semigroup` or `Monoid`.
 160 | public export
 161 | POP (Semigroup . f) [ks] => Semigroup (SOP_ k f [ks]) where
 162 |   MkSOP a <+> MkSOP b = MkSOP $ a <+> b
 163 | 
 164 | ||| Sums of products have instances of `Semigroup` and `Monoid`
 165 | ||| only when they consist of a single choice, which must itself be
 166 | ||| a `Semigroup` or `Monoid`.
 167 | public export
 168 | POP (Monoid . f) [ks] => Monoid (SOP_ k f [ks]) where
 169 |   neutral = MkSOP neutral
 170 | 
 171 | private
 172 | mkSOPInjective : MkSOP a = MkSOP b -> a = b
 173 | mkSOPInjective Refl = Refl
 174 | 
 175 | public export
 176 | POP (DecEq . f) kss => DecEq (SOP_ k f kss) where
 177 |   decEq (MkSOP a) (MkSOP b) with (decEq a b)
 178 |     decEq (MkSOP a) (MkSOP a) | Yes Refl   = Yes $ cong MkSOP Refl
 179 |     decEq (MkSOP a) (MkSOP b) | No  contra = No (contra . mkSOPInjective)
 180 | 
 181 | --------------------------------------------------------------------------------
 182 | --          Examples and Tests
 183 | --------------------------------------------------------------------------------
 184 | 
 185 | neutralTest : SOP I [[String, Maybe Int],[()]]
 186 | neutralTest = hcpure Monoid neutral
 187 | 
 188 | hapTest : SOP Maybe [[String,Int]] -> SOP I [[String,Int]]
 189 | hapTest = hap (MkPOP $ [[fromMaybe "foo", const 12]])
 190 |