roc-id 0.3.0.0 → 0.4.0.0

raw patch · 14 files changed

+294/−93 lines, 14 filesdep +finitarydep +finite-typelitsdep +microlensPVP ok

version bump matches the API change (PVP)

Dependencies added: finitary, finite-typelits, microlens

API changes (from Hackage documentation)

Files

• CHANGELOG.md +12/−0
• LICENSE +1/−1
• README.md +7/−1
• components/roc-id-test/Spec.hs +96/−5
• components/roc-id/ROC/ID.hs +47/−42
• components/roc-id/ROC/ID/Digit.hs +9/−4
• components/roc-id/ROC/ID/Digit1289.hs +8/−6
• components/roc-id/ROC/ID/Gender.hs +8/−3
• components/roc-id/ROC/ID/Letter.hs +8/−3
• components/roc-id/ROC/ID/Location.hs +7/−3
• components/roc-id/ROC/ID/Nationality.hs +12/−3
• components/roc-id/ROC/ID/Unchecked.hs +25/−11
• components/roc-id/ROC/ID/Utilities.hs +43/−10
• roc-id.cabal +11/−1

@@ -1,3 +1,15 @@+# 0.4.0.0++- Revised the `Show` instance of `ID` to produce a valid Haskell expression+  when applied to nested values of `ID`.+- Revised the `ID.fromSymbol` function so that users are presented with a+  helpful error if they forget to apply the function to a concrete type.+- Simplified the error handling for `ID.fromText` by merging the `TextTooShort`+  and `TextTooLong` errors into a unified `InvalidLength` error.+- Renamed `ID.checksumDigit` to `ID.checksum`.+- Made `ID` an instance of the `Finitary` type class.+- Made `ID` an instance of the `Generic` type class.+ # 0.3.0.0  - Added support for ARC (Alien Residence Certificate) numbers.

@@ -1,4 +1,4 @@-Copyright Jonathan Knowles (c) 2018–2025+Copyright Jonathan Knowles (c) 2018–2026  All rights reserved. 

@@ -1,5 +1,11 @@ # `roc-id`-<a href="https://jonathanknowles.github.io/roc-id/"><img src="https://img.shields.io/badge/API-Documentation-227755" /></a>++[![Latest Release](+  https://img.shields.io/hackage/v/roc-id?label=Latest%20Release&color=227755+)](https://hackage.haskell.org/package/roc-id)+[![Development Branch](+  https://img.shields.io/badge/Development%20Branch-API%20Documentation-225577+)](https://jonathanknowles.github.io/roc-id/)  This package provides a [Haskell](https://www.haskell.org/) implementation of the ROC (Taiwan) Uniform Identification Number (中華民國統一證號) format.

@@ -1,6 +1,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-}@@ -17,6 +18,10 @@   ( NonEmpty ((:|)) ) import Data.Text   ( Text )+import Lens.Micro+  ( Lens', lens, set )+import Lens.Micro.Extras+  ( view ) import ROC.ID   ( ID (..) ) import ROC.ID.CharIndex@@ -36,10 +41,11 @@ import ROC.ID.Nationality   ( Nationality (..) ) import Test.Hspec-  ( describe, hspec, it, shouldBe, shouldSatisfy )+  ( Spec, describe, hspec, it, shouldBe, shouldSatisfy ) import Test.QuickCheck   ( Arbitrary (..)   , NonEmptyList (..)+  , Property   , arbitraryBoundedEnum   , choose   , elements@@ -47,12 +53,14 @@   , property   , shrinkBoundedEnum   , shrinkMap+  , (===)   ) import Test.QuickCheck.Classes   ( boundedEnumLaws, eqLaws, numLaws, ordLaws, showLaws, showReadLaws ) import Test.QuickCheck.Classes.Hspec   ( testLawsMany ) +import qualified Data.Finitary as Finitary import qualified Data.Set.NonEmpty as NESet import qualified Data.Text as T import qualified ROC.ID as ID@@ -130,6 +138,48 @@         , showReadLaws         ] +  describe "Finitary instances" $ do++    describe "ID" $ do++      let start    = Finitary.start    @ID+          end      = Finitary.end      @ID+          previous = Finitary.previous @ID+          next     = Finitary.next     @ID++      it "previous start" $+          previous start+            `shouldBe` Nothing++      it "start" $+          start+            `shouldBe` ID.fromSymbol @"A100000001"++      it "next start" $+          next start+            `shouldBe` Just (ID.fromSymbol @"A100000010")++      it "previous end" $+          previous end+            `shouldBe` Just (ID.fromSymbol @"Z999999987")++      it "end" $+          end+            `shouldBe` ID.fromSymbol @"Z999999996"++      it "next end" $+          next end+            `shouldBe` Nothing++  describe "ID attribute getters and setters" $ do++    describe "Gender" $+      checkLensLaws gender+    describe "Location" $+      checkLensLaws location+    describe "Nationality" $+      checkLensLaws nationality+   describe "ID.fromText" $ do      it "successfully parses known-valid identification numbers" $@@ -144,12 +194,12 @@       property $ \(i :: ID) n -> do         let newLength = n `mod` 10         let invalidID = T.take newLength $ ID.toText i-        ID.fromText invalidID `shouldBe` Left ID.TextTooShort+        ID.fromText invalidID `shouldBe` Left ID.InvalidLength      it "does not parse identification numbers that are too long" $       property $ \(i :: ID) (NonEmpty s) -> do         let invalidID = ID.toText i <> T.pack s-        ID.fromText invalidID `shouldBe` Left ID.TextTooLong+        ID.fromText invalidID `shouldBe` Left ID.InvalidLength      it "does not parse identification numbers with invalid location codes" $       property $ \(i :: ID) (c :: Int) -> do@@ -170,7 +220,7 @@     it "does not parse identification numbers with invalid checksums" $       property $ \(i :: ID) (c :: Int) -> do         let invalidChecksumDigit = intToDigit $-              ((c `mod` 9) + fromEnum (ID.checksumDigit i) + 1) `mod` 10+              ((c `mod` 9) + fromEnum (ID.checksum i) + 1) `mod` 10         let invalidID =               T.take 9 (ID.toText i) <> T.pack [invalidChecksumDigit]         ID.fromText invalidID `shouldBe` Left ID.InvalidChecksum@@ -193,7 +243,48 @@               replaceCharAt invalidCharIndex 'x' (ID.toText i)               <>               T.pack trailingExcess-        ID.fromText textInvalid `shouldBe` Left ID.TextTooLong+        ID.fromText textInvalid `shouldBe` Left ID.InvalidLength++checkLensLaws+  :: forall i v. (Arbitrary i, Arbitrary v, Eq i, Eq v, Show i, Show v)+  => Lens' i v+  -> Spec+checkLensLaws l =+  do+    it "Finality"+      $ property lensLawFinality+    it "Idempotence"+      $ property lensLawIdempotence+    it "Invertibility"+      $ property lensLawInvertibility+    it "Reversibility"+      $ property lensLawReversibility+    it "Stability"+      $ property lensLawStability+  where+    lensLawFinality :: i -> v -> v -> Property+    lensLawFinality i v1 v2 = set l v2 (set l v1 i) === set l v2 i++    lensLawIdempotence :: i -> v -> Property+    lensLawIdempotence i v = set l v (set l v i) === set l v i++    lensLawInvertibility :: i -> v -> Property+    lensLawInvertibility i v = view l (set l v i) === v++    lensLawReversibility :: i -> v -> Property+    lensLawReversibility i v = set l (view l i) (set l v i) === i++    lensLawStability :: i -> Property+    lensLawStability i = set l (view l i) i === i++gender :: Lens' ID Gender+gender = lens ID.getGender (flip ID.setGender)++location :: Lens' ID Location+location = lens ID.getLocation (flip ID.setLocation)++nationality :: Lens' ID Nationality+nationality = lens ID.getNationality (flip ID.setNationality)  -- | Replaces a character at a specific position. --

@@ -1,5 +1,8 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -20,7 +23,7 @@   , toText    -- * Validity-  , checksumDigit+  , checksum    -- * Generation   , generate@@ -41,10 +44,14 @@   ( MonadRandom ) import Data.Bifunctor   ( Bifunctor (first) )+import Data.Finitary+  ( Finitary ) import Data.Proxy   ( Proxy (Proxy) ) import Data.Text   ( Text )+import GHC.Generics+  ( Generic ) import GHC.TypeLits   ( Symbol, symbolVal ) import ROC.ID.CharIndex@@ -64,24 +71,20 @@ import ROC.ID.Nationality   ( Nationality (..) ) import ROC.ID.Unchecked-  ( UncheckedID (UncheckedID)-  , ValidID-  )+  ( UncheckedID (UncheckedID), ValidID ) import ROC.ID.Utilities-  ( guard )+  ( guard, randomFinitary ) import Text.Read-  ( Lexeme (Ident, Symbol, Punc), Read (readPrec), lexP, parens )+  ( Lexeme (Ident, Symbol, Punc), Read (readPrec), lexP, parens, prec )  import qualified Data.Text as T-import qualified ROC.ID.Digit as Digit-import qualified ROC.ID.Digit1289 as Digit1289-import qualified ROC.ID.Letter as Letter import qualified ROC.ID.Location as Location import qualified ROC.ID.Unchecked as U  -- | -- $setup -- >>> :set -XDataKinds+-- >>> :set -XOverloadedStrings -- >>> :set -XTypeApplications -- >>> import ROC.ID -- >>> import qualified ROC.ID as ID@@ -99,7 +102,7 @@ -- To guarantee correctness, an 'ID' value does __not__ store the terminal -- checksum digit of the identification number it represents. ----- To compute the checksum digit, use 'checksumDigit'.+-- To compute the checksum digit, use 'checksum'. -- data ID = ID   { c0 :: !Letter@@ -112,10 +115,11 @@   , c7 :: !Digit   , c8 :: !Digit   }-  deriving (Eq, Ord)+  deriving stock (Eq, Ord, Generic)+  deriving anyclass Finitary  instance Read ID where-  readPrec = parens $ do+  readPrec = parens $ prec 10 $ do     Ident  "ID"         <- lexP     Symbol "."          <- lexP     Ident  "fromSymbol" <- lexP@@ -123,8 +127,9 @@     unsafeFromText <$> readPrec  instance Show ID where-  showsPrec _ s =-    showString "ID.fromSymbol @" . shows (toText s)+  showsPrec d s =+    showParen (d > 10) $+      showString "ID.fromSymbol @" . shows (toText s)  -------------------------------------------------------------------------------- -- Construction@@ -187,14 +192,29 @@ --       Character at this position must be a digit in the range [0 .. 9]. -- ... --+-- === Missing or empty symbols+--+-- >>> ID.fromSymbol+-- ...+-- ... Expected a type-level symbol of the form "A123456789".+-- ...+--+-- >>> ID.fromSymbol @""+-- ...+-- ... Expected a type-level symbol of the form "A123456789".+-- ...+-- fromSymbol :: forall (s :: Symbol). ValidID s => ID fromSymbol = unsafeFromText $ T.pack $ symbolVal $ Proxy @s  -- | Attempts to construct an 'ID' from 'Text'. -- -- The input must be exactly 10 characters in length and of the form--- __@A123456789@__.+-- __@A123456789@__: --+-- >>> ID.fromText "A123456789"+-- Right (ID.fromSymbol @"A123456789")+-- -- More precisely, the input must match the regular expression -- __@^[A-Z][1289][0-9]{8}$@__, and the resultant ID must have a valid -- checksum.@@ -212,12 +232,10 @@   where     fromUncheckedError :: U.FromTextError -> FromTextError     fromUncheckedError = \case-      U.TextTooShort ->-        TextTooShort-      U.TextTooLong ->-        TextTooLong       U.InvalidChar i r ->         InvalidChar i r+      U.InvalidLength ->+        InvalidLength  unsafeFromText :: Text -> ID unsafeFromText t =@@ -229,23 +247,20 @@ -- data FromTextError -  = TextTooShort-  -- ^ Indicates that the input text is too short.--  | TextTooLong-  -- ^ Indicates that the input text is too long.--  | InvalidChar CharIndex CharSet+  = InvalidChar CharIndex CharSet   -- ^ Indicates that the input text contains a character that is not allowed.   ---  --   - `CharIndex` specifies the position of the offending character.+  --   - `CharIndex` specifies the position of the invalid character.   --   - `CharSet` specifies the set of characters allowed at that position.    | InvalidChecksum   -- ^ Indicates that the parsed identification number has an invalid checksum. -  deriving (Eq, Ord, Show)+  | InvalidLength+  -- ^ Indicates that the input text has an invalid length. +  deriving stock (Eq, Ord, Show)+ -------------------------------------------------------------------------------- -- Conversion --------------------------------------------------------------------------------@@ -269,8 +284,8 @@  -- | Computes the terminal checksum digit of an 'ID'. ---checksumDigit :: ID -> Digit-checksumDigit (ID u0 u1 u2 u3 u4 u5 u6 u7 u8) =+checksum :: ID -> Digit+checksum (ID u0 u1 u2 u3 u4 u5 u6 u7 u8) =   negate $ U.checksum (UncheckedID u0 u1 u2 u3 u4 u5 u6 u7 u8 0)  --------------------------------------------------------------------------------@@ -280,17 +295,7 @@ -- | Generates a random 'ID'. -- generate :: MonadRandom m => m ID-generate =-  ID-    <$> Letter.generate-    <*> Digit1289.generate-    <*> Digit.generate-    <*> Digit.generate-    <*> Digit.generate-    <*> Digit.generate-    <*> Digit.generate-    <*> Digit.generate-    <*> Digit.generate+generate = randomFinitary  -------------------------------------------------------------------------------- -- Inspection@@ -358,4 +363,4 @@  toUnchecked :: ID -> UncheckedID toUnchecked i@(ID u0 u1 u2 u3 u4 u5 u6 u7 u8) =-  UncheckedID u0 u1 u2 u3 u4 u5 u6 u7 u8 (checksumDigit i)+  UncheckedID u0 u1 u2 u3 u4 u5 u6 u7 u8 (checksum i)

@@ -1,5 +1,7 @@ {-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-}@@ -16,12 +18,14 @@  import Control.Monad.Random   ( MonadRandom )+import Data.Finitary+  ( Finitary ) import GHC.Generics   ( Generic ) import GHC.TypeNats   ( Nat ) import ROC.ID.Utilities-  ( maybeBoundedEnum, randomBoundedEnum )+  ( maybeFinitary, randomFinitary ) import Text.Read   ( Read (readPrec), readMaybe ) @@ -34,7 +38,8 @@ -- data Digit   = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9-  deriving (Bounded, Enum, Eq, Generic, Ord)+  deriving stock (Bounded, Enum, Eq, Generic, Ord)+  deriving anyclass Finitary  -- | Arithmetic modulo 10. --@@ -56,7 +61,7 @@ -- The 'Char' must be a decimal digit in the range @0@ to @9@. -- fromChar :: Char -> Maybe Digit-fromChar c = readMaybe [c] >>= maybeBoundedEnum+fromChar c = readMaybe [c] >>= maybeFinitary  -- | Converts a 'Digit' to a decimal digit character. --@@ -73,7 +78,7 @@ -- | Generates a random digit. -- generate :: MonadRandom m => m Digit-generate = randomBoundedEnum+generate = randomFinitary  type family FromChar (c :: Char) :: Maybe Digit where   FromChar '0' = Just D0

@@ -1,5 +1,7 @@ {-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-}@@ -18,6 +20,8 @@  import Control.Monad.Random   ( MonadRandom )+import Data.Finitary+  ( Finitary ) import GHC.Generics   ( Generic ) import GHC.TypeNats@@ -25,16 +29,14 @@ import ROC.ID.Digit   ( Digit (..) ) import ROC.ID.Utilities-  ( randomBoundedEnum )+  ( randomFinitary )  -- | Represents a single decimal digit from the set {@1@, @2@, @8@, @9@}. -- data Digit1289   = D1289_1 | D1289_2 | D1289_8 | D1289_9-  deriving (Bounded, Enum, Eq, Generic, Ord)--instance Show Digit1289 where-  show = (: []) . toChar+  deriving stock (Bounded, Enum, Eq, Generic, Ord, Read, Show)+  deriving anyclass Finitary  -- | Attempts to parse a 'Digit1289' from a character. --@@ -69,7 +71,7 @@ -- | Generates a random 'Digit1289'. -- generate :: MonadRandom m => m Digit1289-generate = randomBoundedEnum+generate = randomFinitary  type family FromChar (c :: Char) :: Maybe Digit1289 where   FromChar '1' = Just D1289_1

@@ -1,4 +1,6 @@+{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} @@ -10,6 +12,8 @@  import Control.Monad.Random.Class   ( MonadRandom (..) )+import Data.Finitary+  ( Finitary ) import Data.Text   ( Text ) import GHC.Generics@@ -17,12 +21,13 @@ import ROC.ID.Language   ( Language (..) ) import ROC.ID.Utilities-  ( randomBoundedEnum )+  ( randomFinitary )  -- | A person's gender, encodable within an ROC identification number. -- data Gender = Male | Female-  deriving (Bounded, Enum, Eq, Generic, Ord, Read, Show)+  deriving stock (Bounded, Enum, Eq, Generic, Ord, Read, Show)+  deriving anyclass Finitary  -- | Prints the specified 'Gender'. --@@ -44,4 +49,4 @@ -- | Generates a random 'Gender'. -- generate :: MonadRandom m => m Gender-generate = randomBoundedEnum+generate = randomFinitary

@@ -1,5 +1,7 @@ {-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} @@ -13,10 +15,12 @@  import Control.Monad.Random.Class   ( MonadRandom (..) )+import Data.Finitary+  ( Finitary ) import GHC.Generics   ( Generic ) import ROC.ID.Utilities-  ( randomBoundedEnum )+  ( randomFinitary ) import Text.Read   ( readMaybe ) @@ -25,7 +29,8 @@ data Letter   = A | B | C | D | E | F | G | H | I | J | K | L | M   | N | O | P | Q | R | S | T | U | V | W | X | Y | Z-  deriving (Bounded, Enum, Eq, Generic, Ord, Read, Show)+  deriving stock (Bounded, Enum, Eq, Generic, Ord, Read, Show)+  deriving anyclass Finitary  -- | Attempts to parse a 'Letter' from a character. --@@ -45,7 +50,7 @@ -- | Generates a random 'Letter'. -- generate :: MonadRandom m => m Letter-generate = randomBoundedEnum+generate = randomFinitary  type family FromChar (c :: Char) :: Maybe Letter where   FromChar 'A' = Just A; FromChar 'N' = Just N

@@ -1,3 +1,4 @@+{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}@@ -14,6 +15,8 @@  import Control.Monad.Random.Class   ( MonadRandom (..) )+import Data.Finitary+  ( Finitary ) import Data.Text   ( Text ) import GHC.Generics@@ -22,11 +25,11 @@   ( Language (..) ) import ROC.ID.Letter   ( Letter (..) )+import ROC.ID.Utilities+  ( randomFinitary ) import Text.Read   ( Lexeme (Ident, Symbol), Read (readPrec), lexP, parens ) -import qualified ROC.ID.Letter as Letter- -- | Represents a location, encodable within an ROC identification number. -- -- == Location codes@@ -102,6 +105,7 @@ newtype Location = Location Letter   deriving stock (Eq, Generic, Ord)   deriving newtype (Bounded, Enum)+  deriving anyclass Finitary  instance Read Location where   readPrec = parens $ do@@ -191,4 +195,4 @@ -- | Generates a random 'Location'. -- generate :: MonadRandom m => m Location-generate = Location <$> Letter.generate+generate = randomFinitary

@@ -1,3 +1,7 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}+ module ROC.ID.Nationality   ( Nationality (..)   , generate@@ -6,15 +10,20 @@  import Control.Monad.Random.Class   ( MonadRandom (..) )+import Data.Finitary+  ( Finitary )+import GHC.Generics+  ( Generic ) import ROC.ID.Utilities-  ( randomBoundedEnum )+  ( randomFinitary )  -- | Specifies a person's nationality. -- data Nationality = National | NonNational-  deriving (Bounded, Enum, Eq, Ord, Read, Show)+  deriving stock (Bounded, Enum, Eq, Ord, Generic, Read, Show)+  deriving anyclass Finitary  -- | Generates a random 'Nationality'. -- generate :: MonadRandom m => m Nationality-generate = randomBoundedEnum+generate = randomFinitary

@@ -31,6 +31,8 @@   ( NonEmpty ((:|)) ) import Data.Text   ( Text )+import Data.Type.Bool+  ( If ) import Data.Type.Equality   ( type (==) ) import GHC.TypeError@@ -38,7 +40,7 @@ import GHC.TypeLits   ( AppendSymbol, KnownSymbol, Symbol ) import GHC.TypeNats-  ( Mod, Nat, type (+) )+  ( CmpNat, Mod, Nat, type (+) ) import ROC.ID.CharIndex   ( CharIndex (..) ) import ROC.ID.CharSet@@ -50,7 +52,7 @@ import ROC.ID.Letter   ( Letter (..) ) import ROC.ID.Utilities-  ( FromJust, Fst, ReplicateChar, Snd, SymbolToCharList, guard )+  ( FromJust, Fst, ReplicateChar, Snd, SymbolLength, SymbolToCharList, guard )  import qualified Data.Set.NonEmpty as NESet import qualified Data.Text as T@@ -88,16 +90,15 @@   )  data FromTextError-  = TextTooShort-  | TextTooLong-  | InvalidChar CharIndex CharSet+  = InvalidChar CharIndex CharSet+  | InvalidLength   deriving stock (Eq, Ord, Read, Show)  type Parser a = Text -> Either FromTextError (Text, a)  fromText :: Text -> Either FromTextError UncheckedID fromText text0 = do-    when (T.length text0 > 10) $ Left TextTooLong+    when (T.length text0 > 10) $ Left InvalidLength     (text1,  c0                             ) <- parseLetter    text0     (text2,  c1                             ) <- parseDigit1289 text1     (_____, (c2, c3, c4, c5, c6, c7, c8, c9)) <- parseDigits    text2@@ -105,13 +106,13 @@   where     parseLetter :: Parser Letter     parseLetter text = do-      (char, remainder) <- guard TextTooShort $ T.uncons text+      (char, remainder) <- guard InvalidLength $ T.uncons text       letter <- guard (InvalidChar 0 (CharRange 'A' 'Z')) (Letter.fromChar char)       pure (remainder, letter)      parseDigit1289 :: Parser Digit1289     parseDigit1289 text = do-      (char, remainder) <- guard TextTooShort $ T.uncons text+      (char, remainder) <- guard InvalidLength $ T.uncons text       digit1289 <- guard         (InvalidChar 1 (CharSet $ NESet.fromList $ '1' :| ['2', '8', '9']))         (Digit1289.fromChar char)@@ -121,7 +122,7 @@     parseDigits text = do         let (chars, remainder) = T.splitAt 8 text         digitList <- traverse parseIndexedDigit (zip [2 ..] $ T.unpack chars)-        digitTuple <- guard TextTooShort (listToTuple8 digitList)+        digitTuple <- guard InvalidLength (listToTuple8 digitList)         pure (remainder, digitTuple)       where         parseIndexedDigit (i, c) =@@ -162,7 +163,7 @@ data ChecksumValidity   = ChecksumValid   | ChecksumInvalid-  deriving (Eq, Show)+  deriving stock (Eq, Show)  checksumValidity :: UncheckedID -> ChecksumValidity checksumValidity u =@@ -297,5 +298,18 @@  type ValidID s =   ( KnownSymbol s-  , ChecksumValid (SymbolToId s)+  , ChecksumValid (SymbolToId (ConcreteSymbol s))   ) :: Constraint++-- | Ensures the existence of a concrete symbol, or else raises a type error.+--+type family ConcreteSymbol (s :: Symbol) :: Symbol where+  -- If we can compute the symbol's length, then we have a concrete symbol.+  ConcreteSymbol s =+    If+      (CmpNat (SymbolLength s) 0 == GT)+      s+      (TypeError (TypeError.Text ConcreteSymbolError))++type ConcreteSymbolError =+  "Expected a type-level symbol of the form \"A123456789\"."

@@ -1,6 +1,8 @@+{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}@@ -9,24 +11,45 @@  import Control.Monad.Random.Class   ( MonadRandom (..) )+import Data.Finitary+  ( Finitary (fromFinite), Cardinality )+import Data.Finite+  ( packFinite )+import Data.Maybe+  ( fromMaybe )+import Data.Proxy+  ( Proxy (Proxy) ) import GHC.TypeLits-  ( Symbol, UnconsSymbol, ConsSymbol )+  ( Symbol, UnconsSymbol, ConsSymbol, type (<=), type (+) ) import GHC.TypeNats-  ( Nat, type (-) )+  ( Nat, type (-), natVal )+import Numeric.Natural+  ( Natural ) +cardinality :: forall a. Finitary a => Natural+cardinality = natVal $ Proxy @(Cardinality a)+ guard :: x -> Maybe y -> Either x y guard x = maybe (Left x) Right -maybeBoundedEnum :: forall a. (Bounded a, Enum a) => Int -> Maybe a-maybeBoundedEnum i-  | i < fromEnum (minBound :: a) = Nothing-  | i > fromEnum (maxBound :: a) = Nothing-  | otherwise                    = pure $ toEnum i+maybeFinitary :: forall a. Finitary a => Natural -> Maybe a+maybeFinitary = fmap fromFinite . packFinite . fromIntegral @Natural @Integer -randomBoundedEnum :: forall m a. (MonadRandom m, Bounded a, Enum a) => m a-randomBoundedEnum =-  toEnum <$> getRandomR (fromEnum (minBound :: a), fromEnum (maxBound :: a))+randomFinitary+  :: forall m a. (MonadRandom m, Finitary a, 1 <= Cardinality a) => m a+randomFinitary =+    fromMaybe failure . maybeFinitary <$> randomNatural (0, cardinality @a - 1)+  where+    failure = error "randomFinitary: unexpected out-of-bounds value" +randomNatural :: MonadRandom m => (Natural, Natural) -> m Natural+randomNatural (lo, hi) =+  fromIntegral @Integer @Natural <$>+    getRandomR+      ( fromIntegral @Natural @Integer lo+      , fromIntegral @Natural @Integer hi+      )+ type family FromJust (m :: Maybe a) e where   FromJust Nothing e = e   FromJust (Just a) _ = a@@ -36,6 +59,16 @@  type family Snd (t :: (a, a)) :: a where   Snd '(_, y) = y++type family ListLength (as :: [a]) :: Nat where+  ListLength as = ListLengthInner 0 as++type family ListLengthInner (n :: Nat) (as :: [a]) :: Nat where+  ListLengthInner n '[] = n+  ListLengthInner n (a : as) = ListLengthInner (n + 1) as++type family SymbolLength (s :: Symbol) :: Nat where+  SymbolLength s = ListLength (SymbolToCharList s)  type family     SymbolToCharList (s :: Symbol) :: [Char]

@@ -1,6 +1,6 @@ cabal-version:  3.0 name:           roc-id-version:        0.3.0.0+version:        0.4.0.0 synopsis:       Implementation of the ROC (Taiwan) Uniform ID Number format. category:       Identification homepage:       https://github.com/jonathanknowles/roc-id#readme@@ -43,8 +43,14 @@     build-depends:base                      >= 4.17.2.1     && < 4.22 common dependency-doctest     build-depends:doctest                   >= 0.24.2       && < 0.25+common dependency-finitary+    build-depends:finitary                  >= 2.2.0.0      && < 2.3+common dependency-finite-typelits+    build-depends:finite-typelits           >= 0.2.1.0      && < 0.3 common dependency-hspec     build-depends:hspec                     >= 2.5.5        && < 2.12+common dependency-microlens+    build-depends:microlens                 >= 0.5.0.0      && < 0.6 common dependency-MonadRandom     build-depends:MonadRandom               >= 0.5.1.1      && < 0.7 common dependency-nonempty-containers@@ -68,6 +74,8 @@ library   import:     , dependency-base+    , dependency-finitary+    , dependency-finite-typelits     , dependency-MonadRandom     , dependency-nonempty-containers     , dependency-text@@ -93,8 +101,10 @@ test-suite roc-id-test   import:     , dependency-base+    , dependency-finitary     , dependency-hspec     , dependency-MonadRandom+    , dependency-microlens     , dependency-nonempty-containers     , dependency-QuickCheck     , dependency-quickcheck-classes