[Git][ghc/ghc][master] Explain the auxiliary functions of permutations

[Marge Bot (@marge-bot)]

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC


Commits:
21bedd84 by Facundo Domínguez at 2023-01-03T23:27:30-05:00
Explain the auxiliary functions of permutations

- - - - -


1 changed file:

- libraries/base/Data/OldList.hs


Changes:

=====================================
libraries/base/Data/OldList.hs
=====================================
@@ -1266,15 +1266,42 @@ permutations :: [a] -> [[a]]
 -- Related discussions:
 -- * https://mail.haskell.org/pipermail/haskell-cafe/2021-December/134920.html
 -- * https://mail.haskell.org/pipermail/libraries/2007-December/008788.html
+--
+-- Verification of the equivalences of the auxiliary functions with Liquid Haskell:
+-- https://github.com/ucsd-progsys/liquidhaskell/blob/b86fb5b/tests/ple/pos/Permutations.hs
 permutations xs0 = xs0 : perms xs0 []
   where
+    -- | @perms ts is@ is equivalent to
+    --
+    -- > concat
+    -- >   [ interleave {(ts!!n)} {(drop (n+1)} ts) xs []
+    -- >   | n <- [0..length ts - 1]
+    -- >   , xs <- permutations (reverse (take n ts) ++ is)
+    -- >   ]
+    --
+    -- @{(ts!!n)}@ and @{(drop (n+1)}@ denote the values of variables @t@ and @ts@ which
+    -- appear free in the definition of @interleave@ and @interleave'@.
     perms :: forall a. [a] -> [a] -> [[a]]
     perms []     _  = []
     perms (t:ts) is = foldr interleave (perms ts (t:is)) (permutations is)
       where
+        -- @interleave {t} {ts} xs r@ is equivalent to
+        --
+        -- > [ insertAt n t xs ++ ts | n <- [0..length xs - 1] ] ++ r
+        --
+        -- where
+        --
+        -- > insertAt n y xs = take n xs ++ y : drop n xs
+        --
         interleave :: [a] -> [[a]] -> [[a]]
         interleave xs r = let (_,zs) = interleave' id xs r in zs
 
+        -- @interleave' f ys r@ is equivalent to
+        --
+        -- > ( ys ++ ts
+        -- > , [ f (insertAt n t ys ++ ts) | n <- [0..length ys - 1] ] ++ r
+        -- > )
+        --
         interleave' :: ([a] -> b) -> [a] -> [b] -> ([a], [b])
         interleave' _ []     r = (ts, r)
         interleave' f (y:ys) r = let (us,zs) = interleave' (f . (y:)) ys r



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/21bedd84f2cde6aa17d09c610a2a309f3e2a7f10

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/21bedd84f2cde6aa17d09c610a2a309f3e2a7f10
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230103/5c84f728/attachment-0001.html>