Control.DivideAndConquer


   0 | ||| The content of this module is based on the paper
   1 | ||| A Type-Based Approach to Divide-And-Conquer Recursion in Coq
   2 | ||| by Pedro Abreu, Benjamin Delaware, Alex Hubers, Christa Jenkins,
   3 | ||| J. Garret Morris, and Aaron Stump
   4 | ||| https://doi.org/10.1145/3571196
   5 | |||
   6 | ||| The original paper relies on Coq's impredicative Set axiom,
   7 | ||| something we don't have access to in Idris 2. We can however
   8 | ||| reproduce the results by ignoring the type levels
   9 | 
  10 | module Control.DivideAndConquer
  11 | 
  12 | %default total
  13 | 
  14 | namespace Section4Sub1
  15 | 
  16 |   public export
  17 |   data ListF : (a, x : Type) -> Type where
  18 |     Nil : ListF a x
  19 |     (::) : a -> x -> ListF a x
  20 | 
  21 |   lengthAlg : ListF a Nat -> Nat
  22 |   lengthAlg [] = 0
  23 |   lengthAlg (_ :: n) = S n
  24 | 
  25 |   public export
  26 |   Functor (ListF a) where
  27 |     map f [] = []
  28 |     map f (x :: xs) = x :: f xs
  29 | 
  30 | namespace Section6Sub1
  31 | 
  32 |   public export
  33 |   -- Only accepted because there is currently no universe check
  34 |   data Mu : (Type -> Type) -> Type where
  35 |     MkMu : forall r. (r -> Mu f) -> f r -> Mu f
  36 | 
  37 |   public export
  38 |   inMu : f (Mu f) -> Mu f
  39 |   inMu = MkMu id
  40 | 
  41 |   public export
  42 |   outMu : Functor f => Mu f -> f (Mu f)
  43 |   outMu (MkMu f d) = f <$> d
  44 | 
  45 |   public export
  46 |   fold : Functor f => (f a -> a) -> Mu f -> a
  47 |   fold alg (MkMu f r) = alg (assert_total (fold alg . f <$> r))
  48 | 
  49 | namespace Section4Sub1
  50 | 
  51 |   list : Type -> Type
  52 |   list = Mu . ListF
  53 | 
  54 |   namespace Smart
  55 | 
  56 |     Nil : list a
  57 |     Nil = inMu []
  58 | 
  59 |     (::) : a -> list a -> list a
  60 |     x :: xs = inMu (x :: xs)
  61 | 
  62 |     fromList : List a -> list a
  63 |     fromList = foldr (::) []
  64 | 
  65 |     toList : list a -> List a
  66 |     toList = fold $ \case
  67 |       [] => []
  68 |       (x :: xs) => x :: xs
  69 | 
  70 | namespace Section4Sub2
  71 | 
  72 |   public export
  73 |   KAlg : Type
  74 |   KAlg = (Type -> Type) -> Type
  75 | 
  76 |   public export
  77 |   0 Mono : (KAlg -> KAlg) -> Type
  78 |   Mono f
  79 |     = forall a, b.
  80 |       (forall x.   a x ->   b x) ->
  81 |       (forall x. f a x -> f b x)
  82 | 
  83 |   public export
  84 |   data Mu : (KAlg -> KAlg) -> KAlg where
  85 |     MkMu : (forall x. a x -> Mu f x) ->
  86 |            (forall x. f a x -> Mu f x)
  87 | 
  88 |   public export
  89 |   inMu : f (Mu f) x -> Mu f x
  90 |   inMu = MkMu id
  91 | 
  92 |   public export
  93 |   outMu : Mono f -> Mu f x -> f (Mu f) x
  94 |   outMu m (MkMu f d) = m f d
  95 | 
  96 |   parameters (0 f : Type -> Type)
  97 | 
  98 |     public export
  99 |     0 FoldT : KAlg -> Type -> Type
 100 |     FoldT a r
 101 |       = forall x.
 102 |         Functor x =>
 103 |         a x -> r -> x r
 104 | 
 105 |     public export
 106 |     0 SAlgF : KAlg -> (Type -> Type) -> Type
 107 |     SAlgF a x
 108 |       = forall p, r.
 109 |         (r -> p) ->
 110 |         FoldT a r ->
 111 |         (f r -> p) ->
 112 |         (r -> x r) ->
 113 |         f r -> x p
 114 | 
 115 | 
 116 |     public export
 117 |     0 SAlg : (Type -> Type) -> Type
 118 |     SAlg = Mu SAlgF
 119 | 
 120 |     public export
 121 |     0 AlgF : KAlg -> (Type -> Type) -> Type
 122 |     AlgF a x
 123 |       = forall r.
 124 |         FoldT a r ->
 125 |         FoldT SAlg r ->
 126 |         (r -> x r) ->
 127 |         f r -> x r
 128 | 
 129 |     public export
 130 |     0 Alg : (Type -> Type) -> Type
 131 |     Alg = Mu AlgF
 132 | 
 133 |     public export
 134 |     inSAlg : SAlgF SAlg x -> SAlg x
 135 |     inSAlg = inMu
 136 | 
 137 |     public export
 138 |     monoSAlgF : Mono SAlgF
 139 |     monoSAlgF f salg up sfo = salg up (sfo . f)
 140 | 
 141 |     public export
 142 |     outSAlg : SAlg x -> SAlgF SAlg x
 143 |     outSAlg = outMu monoSAlgF
 144 | 
 145 |     public export
 146 |     inAlg : AlgF Alg x -> Alg x
 147 |     inAlg = inMu
 148 | 
 149 |     public export
 150 |     monoAlgF : Mono AlgF
 151 |     monoAlgF f alg fo = alg (fo . f)
 152 | 
 153 |     public export
 154 |     outAlg : Alg x -> AlgF Alg x
 155 |     outAlg = outMu monoAlgF
 156 | 
 157 | namespace Section6Sub2
 158 | 
 159 |   parameters (0 f : Type -> Type)
 160 | 
 161 |     public export
 162 |     0 DcF : Type -> Type
 163 |     DcF a = forall x. Functor x => Alg f x -> x a
 164 | 
 165 |     public export
 166 |     functorDcF : Functor DcF
 167 |     functorDcF = MkFunctor $ \ f, dc, alg => map f (dc alg)
 168 | 
 169 |     public export
 170 |     0 Dc : Type
 171 |     Dc = Mu DcF
 172 | 
 173 |     public export
 174 |     fold : FoldT f (Alg f) Dc
 175 |     fold alg dc = outMu @{functorDcF} dc alg
 176 | 
 177 |     public export
 178 |     record RevealT (x : Type -> Type) (r : Type) where
 179 |       constructor MkRevealT
 180 |       runRevealT : (r -> Dc) -> x Dc
 181 | 
 182 |     public export %hint
 183 |     functorRevealT : Functor (RevealT x)
 184 |     functorRevealT = MkFunctor $ \ f, t =>
 185 |       MkRevealT (\ g => runRevealT t (g . f))
 186 | 
 187 |     public export
 188 |     promote : Functor x => SAlg f x -> Alg f (RevealT x)
 189 |     promote salg
 190 |       = inAlg f $ \ fo, sfo, rec, fr =>
 191 |         MkRevealT $ \ reveal =>
 192 |         let abstIn := \ fr => inMu (\ alg => reveal <$> outAlg f alg fo sfo (fo alg) fr) in
 193 |         outSAlg f salg reveal sfo abstIn (sfo salg) fr
 194 | 
 195 |     public export
 196 |     sfold : FoldT f (SAlg f) Dc
 197 |     sfold salg dc = runRevealT (fold (promote salg) dc) id
 198 | 
 199 |     public export
 200 |     inDc : f Dc -> Dc
 201 |     inDc d = inMu (\ alg => outAlg f alg fold sfold (fold alg) d)
 202 | 
 203 |     out : Functor f => FoldT f (SAlg f) r -> r -> f r
 204 |     out sfo = sfo (inSAlg f (\ up, _, _, _ => map up))
 205 | 
 206 | namespace Section5Sub1
 207 | 
 208 |   public export
 209 |   0 list : Type -> Type
 210 |   list a = Dc (ListF a)
 211 | 
 212 |   namespace Smart
 213 | 
 214 |     public export
 215 |     Nil : list a
 216 |     Nil = inDc (ListF a) []
 217 | 
 218 |     public export
 219 |     (::) : a -> list a -> list a
 220 |     x :: xs = inDc (ListF a) (x :: xs)
 221 | 
 222 |     public export
 223 |     fromList : List a -> list a
 224 |     fromList = foldr (::) []
 225 | 
 226 |   public export
 227 |   0 SpanF : Type -> Type -> Type
 228 |   SpanF a x = (List a, x)
 229 | 
 230 |   SpanSAlg : (a -> Bool) -> SAlg (ListF a) (SpanF a)
 231 |   SpanSAlg p = inSAlg (ListF a) $ \up, sfo, abstIn, span, xs =>
 232 |     case xs of
 233 |       [] => ([], abstIn xs)
 234 |       (x :: xs') =>
 235 |         if p x
 236 |         then let (r, s) = span xs' in (x :: r, up s)
 237 |         else ([], abstIn xs)
 238 | 
 239 |   export
 240 |   spanr : FoldT (ListF a) (SAlg (ListF a)) r ->
 241 |           (a -> Bool) -> (xs : r) -> SpanF a r
 242 |   spanr sfo p xs = sfo (SpanSAlg p) @{MkFunctor mapSnd} xs
 243 | 
 244 |   breakr : FoldT (ListF a) (SAlg (ListF a)) r ->
 245 |            (a -> Bool) ->  (xs : r) -> SpanF a r
 246 |   breakr sfo p = spanr sfo (not . p)
 247 | 
 248 |   WordsByAlg : (a -> Bool) -> Alg (ListF a) (const (List (List a)))
 249 |   WordsByAlg p = inAlg (ListF a) $ \ fo, sfo, wordsBy, xs =>
 250 |     case xs of
 251 |       [] => []
 252 |       (hd :: tl) =>
 253 |         if p hd
 254 |         then wordsBy tl
 255 |         else
 256 |           let (w, rest) = breakr sfo p tl in
 257 |           (hd :: w) :: wordsBy rest
 258 | 
 259 |   wordsBy : (a -> Bool) -> (xs : List a) -> List (List a)
 260 |   wordsBy p = fold (ListF a) @{MkFunctor (const id)} (WordsByAlg p) . fromList
 261 | 
 262 | namespace Section5Sub3
 263 | 
 264 |   data NatF x = Z | S x
 265 | 
 266 |   0 nat : Type
 267 |   nat = Dc NatF
 268 | 
 269 |   fromNat : Nat -> Section5Sub3.nat
 270 |   fromNat Z = inDc NatF Z
 271 |   fromNat (S n) = inDc NatF (S (fromNat n))
 272 | 
 273 |   toNat : Section5Sub3.nat -> Nat
 274 |   toNat = fold NatF @{MkFunctor (const id)} idAlg where
 275 | 
 276 |     idAlg : Alg NatF (const Nat)
 277 |     idAlg = inAlg NatF $ \ fo, sfo, toNat, n =>
 278 |       case n of
 279 |         Z => Z
 280 |         S n' => S (toNat n')
 281 | 
 282 |   zeroSAlg : SAlg NatF Prelude.id
 283 |   zeroSAlg = inSAlg NatF $ \ up, sfo, abstIn, zero, n =>
 284 |     case n of
 285 |       Z => abstIn n
 286 |       S p => up (zero (zero p))
 287 | 
 288 |   export
 289 |   zero : Nat -> Nat
 290 |   zero = toNat . sfold NatF @{MkFunctor id} zeroSAlg . fromNat
 291 | 
 292 | namespace Section5Sub3
 293 | 
 294 |   data TreeF a x = Node a (List x)
 295 | 
 296 |   0 tree : Type -> Type
 297 |   tree a = Dc (TreeF a)
 298 | 
 299 |   node : a -> List (tree a) -> tree a
 300 |   node n ts = inDc (TreeF a) (Node n ts)
 301 | 
 302 |   mirrorAlg : SAlg (TreeF a) Prelude.id
 303 |   mirrorAlg = inSAlg (TreeF a) $ \ up, sfo, abstIn, mirror, t =>
 304 |     case t of Node a ts => abstIn (Node a $ map mirror (reverse ts))
 305 | 
 306 |   mirror : tree a -> tree a
 307 |   mirror = sfold (TreeF a) @{MkFunctor id} mirrorAlg
 308 | 
 309 | namespace Section5Sub4
 310 | 
 311 |   0 MappedT : (a, b : Type) -> Type
 312 |   MappedT a b = forall r. FoldT (ListF a) (SAlg (ListF a)) r -> a -> r -> (b, r)
 313 | 
 314 |   MapThroughAlg : MappedT a b -> Alg (ListF a) (const (List b))
 315 |   MapThroughAlg f = inAlg (ListF a) $ \fo, sfo, mapThrough, xs =>
 316 |     case xs of
 317 |       [] => []
 318 |       hd :: tl =>
 319 |         let (b, rest) = f sfo hd tl in
 320 |         b :: mapThrough rest
 321 | 
 322 |   mapThrough : MappedT a b -> list a -> List b
 323 |   mapThrough f = fold (ListF a) (MapThroughAlg f) @{MkFunctor (const id)}
 324 | 
 325 |   compressSpan : Eq a => MappedT a (Nat, a)
 326 |   compressSpan sfo hd tl
 327 |     = let (pref, rest) = spanr sfo (hd ==) tl in
 328 |       ((S (length pref), hd), rest)
 329 | 
 330 |   runLengthEncoding : Eq a => List a -> List (Nat, a)
 331 |   runLengthEncoding = mapThrough compressSpan . fromList
 332 | 
 333 | namespace Section5Sub5
 334 | 
 335 |   K : Type -> Type
 336 |   K t = t -> Bool
 337 | 
 338 |   MatchT : Type -> Type
 339 |   MatchT t = K t -> Bool
 340 | 
 341 |   data Regex = Zero | Exact Char | Sum Regex Regex | Cat Regex Regex | Plus Regex
 342 | 
 343 |   matchi : (t -> Regex -> MatchT t) -> Regex -> Char -> t -> MatchT t
 344 |   matchi matcher Zero c cs k = False
 345 |   matchi matcher (Exact c') c cs k = (c == c') && k cs
 346 |   matchi matcher (Sum r1 r2) c cs k = matchi matcher r1 c cs k || matchi matcher r2 c cs k
 347 |   matchi matcher (Cat r1 r2) c cs k = matchi matcher r1 c cs (\ cs => matcher cs r2 k)
 348 |   matchi matcher (Plus r) c cs k = matchi matcher r c cs (\ cs => k cs || matcher cs (Plus r) k)
 349 | 
 350 |   MatcherF : Type -> Type
 351 |   MatcherF t = Regex -> MatchT t
 352 | 
 353 |   functorMatcherF : Functor MatcherF
 354 |   functorMatcherF = MkFunctor (\ f, t, r, p => t r (p . f))
 355 | 
 356 |   MatcherAlg : Alg (ListF Char) MatcherF
 357 |   MatcherAlg = inAlg (ListF Char) $ \ fo, sfo, matcher, s =>
 358 |     case s of
 359 |       [] =>  \ r, k => False
 360 |       (c :: cs) => \ r => matchi matcher r c cs
 361 | 
 362 |   match : Regex -> String -> Bool
 363 |   match r str = fold (ListF Char) MatcherAlg @{functorMatcherF} chars r isNil
 364 | 
 365 |     where
 366 |       isNil : Mu (DcF (ListF Char)) -> Bool
 367 |       isNil = fold (ListF Char) {x = const Bool} @{MkFunctor (const id)}
 368 |             $ inAlg (ListF Char)
 369 |             $ \fo, sfo, rec, xs => case xs of
 370 |               Nil => True
 371 |               (_ :: _) => False
 372 | 
 373 |       chars : Mu (DcF (ListF Char))
 374 |       chars = fromList (unpack str)
 375 | 
 376 |   export
 377 |   matchExample : Bool
 378 |   matchExample = match (Plus $ Cat (Sum (Exact 'a') (Exact 'b')) (Exact 'a')) "aabaaaba"
 379 | 
 380 | namespace Section5Sub6
 381 | 
 382 |   parameters {0 a : Type} (ltA : a -> a -> Bool)
 383 | 
 384 |     0 PartF : Type -> Type
 385 |     PartF x = a -> (x, x)
 386 | 
 387 |     PartSAlg : SAlg (ListF a) PartF
 388 |     PartSAlg = inSAlg (ListF a) $ \up, sfo, abstIn, partition, d, pivot => case d of
 389 |       [] => let xs = abstIn d in (xs, xs)
 390 |       x :: xs => let (l, r) = partition xs pivot in
 391 |                  if ltA x pivot then (abstIn (x :: l), up r)
 392 |                  else (up l, abstIn (x :: r))
 393 | 
 394 |     partr : (sfo : FoldT (ListF a) (SAlg (ListF a)) r) -> r -> a -> (r, r)
 395 |     partr sfo = sfo @{MkFunctor $ \ f, p, x => bimap f f (p x)} PartSAlg
 396 | 
 397 |     QuickSortAlg : Alg (ListF a) (const (List a))
 398 |     QuickSortAlg = inAlg (ListF a) $ \ fo, sfo, qsort, xs => case xs of
 399 |       [] => []
 400 |       p :: xs => let (l, r) = partr sfo xs p in
 401 |                  qsort l ++ p :: qsort r
 402 | 
 403 |     quicksort : List a -> List a
 404 |     quicksort = fold (ListF a) QuickSortAlg @{MkFunctor (const id)} . fromList
 405 | 
 406 |   export
 407 |   sortExample : String -> String
 408 |   sortExample = pack . quicksort (<=) . unpack
 409 |