Fin 0.2.3.0 → 0.2.4.0

raw patch · 4 files changed

+106/−4 lines, 4 filesdep +algdep +foldable1PVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: alg, foldable1

API changes (from Hackage documentation)

Files

• Data/Fin/List.hs +1/−1
• Data/Fin/Permutation.hs +83/−0
• Data/Fin/Private.hs +9/−0
• Fin.cabal +13/−3

@@ -1,5 +1,5 @@ module Data.Fin.List (Peano, List (..),-                      fromList, uncons, head, tail, init, last, reverse, at, swap, (!!)) where+                      fromList, uncons, head, tail, init, last, reverse, rotate, at, swap, (!!)) where  import Prelude () import Data.Fin.Private

@@ -0,0 +1,83 @@+{-# LANGUAGE TypeApplications #-}++module Data.Fin.Permutation (Permutation, apply, unapply, swap, orbit, cycles) where++import Prelude (Functor (..), Eq (..), Bool (..), ($), (<$>), otherwise, snd, flip, curry, uncurry)+import Algebra+import Control.Category (Category (..))+import Data.Fin+import Data.Fin.List hiding (swap)+import qualified Data.Fin.List as L+import Data.Foldable (elem, minimum, toList)+import Data.List.NonEmpty (NonEmpty (..))+import Data.Natural.Class (Natural (..))+import qualified Data.Peano as P++data Permutation n where+    PZ :: Permutation P.Zero+    PS :: Fin (P.Succ n) -> Permutation n -> Permutation (P.Succ n)++apply :: Permutation n -> List n a -> List n a+apply PZ Nil = Nil+apply (PS Zero p) (a:.as) = a:.apply p as+apply (PS (Succ n) p) (a:.as) = uncurry (:.) $ at n (flip (,) a) (apply p as)++unapply :: Permutation n -> List n a -> List n a+unapply PZ Nil = Nil+unapply (PS Zero p) (a:.as) = a:.unapply p as+unapply (PS (Succ n) p) (a:.as) = unapply (PS Zero p) . uncurry (:.) $ at n (flip (,) a) as++instance Natural n => Semigroup (Permutation n) where+    (<>) = unOp₂ $ natural (Op₂ . curry $ \ (PZ, PZ) -> PZ) $ Op₂ . curry $ \ case+        (PS m p, PS Zero q) -> PS m (p <> q)+        (PS m p, PS n q) -> case invert (PS n (invert p)) of+            PS o r -> case (m, o) of+                (Zero, _) -> PS o (r <> q)+                (_, Zero) -> PS m (r <> q)+                (Succ m, Succ o) -> PS (Succ o) (swap m o <> r <> q)++instance Natural n => Monoid (Permutation n) where+    mempty = natural PZ $ PS Zero mempty++instance Natural n => Group (Permutation n) where+    invert = snd . go+      where+        go :: ∀ n . Permutation n -> (List n (Fin n), Permutation n)+        go PZ = (Nil, PZ)+        go (PS n p) = (ms, PS m q)+          where (ns, q) = go p+                ms@(m:._) = L.swap Zero n $ Zero:.(Succ <$> ns)++swap :: Natural n => Fin n -> Fin n -> Permutation n+swap = unOp₂ $ natural (Op₂ $ \ case) $ Op₂ . curry $ \ case+    (Zero, Zero) -> mempty+    (Succ m, Succ n) -> PS Zero (swap m n)+    (Zero, Succ n) -> PS (Succ n) mempty+    (Succ m, Zero) -> PS (Succ m) mempty++newtype Op₂ a b n = Op₂ { unOp₂ :: a n -> a n -> b n }++orbit :: Natural n => Permutation n -> Fin n -> NonEmpty (Fin n)+orbit p n = case (!! n) <$> iterate (apply p) enum of+    a:<as -> a:|takeWhile (/= a) as++cycles :: ∀ n . Natural n => Permutation (P.Succ n) -> NonEmpty (NonEmpty (Fin (P.Succ n)))+cycles p = nubOn minimum $ orbit p <$> case enum @(P.Succ n) of n:.ns -> n:|toList ns++infixr 5 :<+data Stream a = a :< Stream a+  deriving (Functor)++iterate :: (a -> a) -> a -> Stream a+iterate f a = a :< (f <$> iterate f a)++takeWhile :: (a -> Bool) -> Stream a -> [a]+takeWhile f (a:<as) | f a = a:takeWhile f as+                    | otherwise = []++nubOn :: Eq b => (a -> b) -> NonEmpty a -> NonEmpty a+nubOn f (a:|as) = a:|go [f a] as+  where go _ [] = []+        go bs (a:as) | b `elem` bs = go bs as+                     | otherwise   = a:go (b:bs) as+          where b = f a

@@ -10,10 +10,12 @@ import Data.Ap import Data.Eq import Data.Foldable+import Data.Foldable1 import Data.Function (on) import Data.Functor.Classes import Data.Functor.Compose import qualified Data.List as L+import Data.List.NonEmpty (NonEmpty (..)) import Data.Maybe import Data.Monoid hiding ((<>)) import Data.Natural.Class@@ -156,6 +158,9 @@ instance Natural n => Read1 (List n) where     liftReadPrec rp rl = fromList <$> liftReadPrec rp rl >>= maybe empty pure +instance Natural n => Foldable1 (List (P.Succ n)) where+    toNonEmpty (a:.as) = a:|toList as+ uncons :: List (P.Succ n) a -> (a, List n a) uncons (x:.xs) = (x, xs) @@ -176,6 +181,10 @@ reverse :: List n a -> List n a reverse Nil = Nil reverse xs@(_:._) = liftA2 (:.) last (reverse . init) xs++rotate :: Fin n -> List n a -> List n a+rotate Zero as = as+rotate (Succ n) as = rotate (inj₁ n) $ last as :. init as  (!!) :: List n a -> Fin n -> a Nil !! n = case n of

@@ -1,5 +1,5 @@ name:                Fin-version:             0.2.3.0+version:             0.2.4.0 synopsis:            Finite totally-ordered sets -- description:          license:             BSD3@@ -15,9 +15,12 @@   build-depends:       peano   exposed-modules:     Data.Fin                      , Data.Fin.List+                     , Data.Fin.Permutation   other-modules:       Data.Ap                      , Data.Fin.Private-  build-depends:       base >=4.7 && <5+  build-depends:       alg >=0.2.5 && <0.3+                     , base >=4.7 && <5+                     , foldable1 >=0.1 && <0.2                      , natural-induction >=0.2 && <0.3   default-language:    Haskell2010   default-extensions:  UnicodeSyntax@@ -31,4 +34,11 @@                      , GADTs                      , StandaloneDeriving                      , DeriveFunctor, DeriveFoldable, DeriveTraversable-  ghc-options:         -Wall -Wno-name-shadowing -Wno-unticked-promoted-constructors+  ghc-options:         -Wall -Wcompat -Wredundant-constraints+                       -Wincomplete-record-updates -Wincomplete-uni-patterns+                       -Wno-name-shadowing -Wno-unticked-promoted-constructors+                       -Werror=incomplete-patterns+                       -Werror=incomplete-uni-patterns+                       -Werror=incomplete-record-updates+                       -Werror=missing-fields+                       -Werror=missing-methods