Fin 0.1.0.0 → 0.1.1.0
raw patch · 2 files changed
+104/−3 lines, 2 filesdep +clistdep +natural-induction
Dependencies added: clist, natural-induction
Files
- Data/Fin.hs +90/−1
- Fin.cabal +14/−2
Data/Fin.hs view
@@ -1,10 +1,99 @@-{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}+{-# LANGUAGE TypeApplications #-} module Data.Fin where +import Prelude hiding (iterate)+import Control.Applicative+import Data.Ap+import Data.CList (CList (..))+import Data.Foldable+import Data.Function (on)+import Data.Functor.Compose+import Data.Maybe+import Data.Natural.Class import Data.Peano (Peano) import qualified Data.Peano as P+import Data.Semigroup (Endo (..))+import qualified Numeric.Natural as N+import qualified Text.ParserCombinators.ReadP as Read+import Text.ParserCombinators.ReadPrec (readP_to_Prec)+import Text.Read (Read (..)) data Fin :: Peano -> * where Zero :: Fin (P.Succ n) Succ :: Fin n -> Fin (P.Succ n)++deriving instance Eq (Fin n)+deriving instance Ord (Fin n)+deriving instance Show (Fin n)++instance Read (Fin P.Zero) where readPrec = empty+instance Read (Fin n) => Read (Fin (P.Succ n)) where+ readPrec = Succ <$ string "Succ" <*> readPrec <|> Zero <$ string "Zero"+ where string = readP_to_Prec . pure . Read.string++instance Bounded (Fin (P.Succ P.Zero)) where+ minBound = Zero+ maxBound = Zero++instance Bounded (Fin n) => Bounded (Fin (P.Succ n)) where+ minBound = Zero+ maxBound = Succ maxBound++instance Enum (Fin P.Zero) where+ toEnum _ = error "toEnum @(Fin Zero)"+ fromEnum = \ case+ succ = \ case+ pred = \ case++instance (Natural n, Enum (Fin n)) => Enum (Fin (P.Succ n)) where+ toEnum 0 = Zero+ toEnum n = Succ (toEnum (pred n))+ fromEnum Zero = 0+ fromEnum (Succ n) = succ (fromEnum n)+ enumFrom Zero = Zero : (Succ <$> toList enum)+ enumFrom (Succ n) = (tail . enumFrom . inj₁) n++enum :: Natural n => CList n (Fin n)+enum = ap $ natural (Ap Nil) (Ap (Zero :. (Succ <$> enum)))++instance Num (Fin P.Zero) where+ (+) = \ case+ (*) = \ case+ abs = id+ negate = \ case+ signum = \ case+ fromInteger _ = error "fromInteger @(Fin Zero)"++instance (Natural n, Num (Fin n)) => Num (Fin (P.Succ n)) where+ a + b = toFin $ ((+) @N.Natural `on` fromFin) a b+ a - b = toFin $ ((-) @ Integer `on` fromFin) a b+ a * b = toFin $ ((*) @N.Natural `on` fromFin) a b++ abs = id+ signum = lift₁ . appEndo . getCompose $+ natural @n (Compose . Endo $ \ case) (Compose . Endo $ pure Zero)++ fromInteger = toFin++inj₁ :: Fin n -> Fin (P.Succ n)+inj₁ Zero = Zero+inj₁ (Succ n) = Succ (inj₁ n)++lift₁ :: (Fin m -> Fin n) -> Fin (P.Succ m) -> Fin (P.Succ n)+lift₁ _ Zero = Zero+lift₁ f (Succ n) = Succ (f n)++fromFin :: Integral a => Fin n -> a+fromFin Zero = 0+fromFin (Succ n) = succ (fromFin n)++toFin :: ∀ n a . (Natural n, Integral a) => a -> Fin (P.Succ n)+toFin = fromJust . toFinMay . (`mod` getConst (iterate @n (+1) 1))++toFinMay :: (Natural n, Integral a) => a -> Maybe (Fin (P.Succ n))+toFinMay = getCompose . getCompose . getCompose $+ natural (Compose . Compose . Compose $ \ case 0 -> Just Zero+ _ -> Nothing)+ (Compose . Compose . Compose $ \ case 0 -> Just Zero+ n -> Succ <$> toFinMay (n-1))
Fin.cabal view
@@ -1,5 +1,5 @@ name: Fin-version: 0.1.0.0+version: 0.1.1.0 synopsis: Finite totally-ordered sets -- description: license: BSD3@@ -14,6 +14,18 @@ library build-depends: peano exposed-modules: Data.Fin- other-extensions: GADTs, KindSignatures, DataKinds build-depends: base >=4.7 && <5+ , clist >=0.2 && <0.3+ , natural-induction >=0.2 && <0.3 default-language: Haskell2010+ default-extensions: UnicodeSyntax+ , ScopedTypeVariables+ , LambdaCase+ , EmptyCase+ , PolyKinds+ , DataKinds+ , GADTs+ , FlexibleContexts+ , FlexibleInstances+ , StandaloneDeriving+ ghc-options: -Wall -Wno-unticked-promoted-constructors