summaryrefslogtreecommitdiff
path: root/libraries
diff options
context:
space:
mode:
authorFacundo Domínguez <facundo.dominguez@tweag.io>2022-12-23 23:16:23 -0300
committerMarge Bot <ben+marge-bot@smart-cactus.org>2023-01-03 23:27:30 -0500
commit21bedd84f2cde6aa17d09c610a2a309f3e2a7f10 (patch)
tree6ab35a8f1d9f2c195b79bb31a529675e2cfbd2a6 /libraries
parent62b9a7b23b20f5cf0a2de14251c2096098009f10 (diff)
downloadhaskell-21bedd84f2cde6aa17d09c610a2a309f3e2a7f10.tar.gz
Explain the auxiliary functions of permutations
Diffstat (limited to 'libraries')
-rw-r--r--libraries/base/Data/OldList.hs27
1 files changed, 27 insertions, 0 deletions
diff --git a/libraries/base/Data/OldList.hs b/libraries/base/Data/OldList.hs
index 58b0bce8b2..176c72547c 100644
--- a/libraries/base/Data/OldList.hs
+++ b/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