packages feed

taiwan-id (empty) → 0.0.0.0

raw patch · 20 files changed

+1996/−0 lines, 20 filesdep +MonadRandomdep +QuickCheckdep +basebuild-type:Customsetup-changed

Dependencies added: MonadRandom, QuickCheck, base, doctest, finitary, finite-typelits, hspec, microlens, nonempty-containers, quickcheck-classes, taiwan-id, text

Files

+ CHANGELOG.md view
@@ -0,0 +1,3 @@+# 0.0.0.0++- Initial release.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Jonathan Knowles (c) 2018–2026++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Jonathan Knowles nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,31 @@+# `taiwan-id`++[![Latest Release](+  https://img.shields.io/hackage/v/taiwan-id?label=Latest%20Release&color=227755+)](https://hackage.haskell.org/package/taiwan-id)+[![Development Branch](+  https://img.shields.io/badge/Development%20Branch-API%20Documentation-225577+)](https://jonathanknowles.github.io/taiwan-id/)++This package provides a Haskell implementation of Taiwan's uniform+identification number format.++This number format is used by both National Identification Cards (國民身分證)+and Alien Resident Certificates (外僑居留證) issued by the Republic of China+(ROC) government to individuals, with numbers assigned under each system+occupying disjoint parts of the same identifier space.++Each identification number consists of a single uppercase letter followed by+nine decimal digits, with the final digit serving as a checksum calculated+according to a standard algorithm.++Example: `A123456789`++This package offers functions for validating, decoding, and encoding these+numbers.++For more details, see:++* https://zh.wikipedia.org/wiki/中華民國國民身分證+* https://en.wikipedia.org/wiki/National_identification_card_(Taiwan)+* https://en.wikipedia.org/wiki/Resident_certificate
+ Setup.hs view
@@ -0,0 +1,5 @@+import Distribution.Extra.Doctest+  ( defaultMainWithDoctests )++main :: IO ()+main = defaultMainWithDoctests "taiwan-id-test-docs"
+ components/taiwan-id-test-docs/Main.hs view
@@ -0,0 +1,9 @@+module Main where++import Build_doctests+  ( flags, pkgs, module_sources )+import Test.DocTest+  ( doctest )++main :: IO ()+main = doctest (flags ++ pkgs ++ module_sources)
+ components/taiwan-id-test/Spec.hs view
@@ -0,0 +1,340 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+{- HLINT ignore "Redundant bracket" -}++module Main where++import Data.Bifunctor+  ( Bifunctor (second) )+import Data.Char+  ( intToDigit )+import Data.List.NonEmpty+  ( NonEmpty ((:|)) )+import Data.Text+  ( Text )+import Lens.Micro+  ( Lens', lens, set )+import Lens.Micro.Extras+  ( view )+import Taiwan.ID+  ( ID (..) )+import Taiwan.ID.CharIndex+  ( CharIndex (CharIndex) )+import Taiwan.ID.CharSet+  ( CharSet (..) )+import Taiwan.ID.Digit+  ( Digit (..) )+import Taiwan.ID.Digit1289+  ( Digit1289 (..) )+import Taiwan.ID.Gender+  ( Gender (..) )+import Taiwan.ID.Letter+  ( Letter (..) )+import Taiwan.ID.Location+  ( Location )+import Taiwan.ID.Nationality+  ( Nationality (..) )+import Test.Hspec+  ( Spec, describe, hspec, it, shouldBe, shouldSatisfy )+import Test.QuickCheck+  ( Arbitrary (..)+  , NonEmptyList (..)+  , Property+  , arbitraryBoundedEnum+  , choose+  , elements+  , forAll+  , 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 Taiwan.ID as ID++instance Arbitrary Digit where+  arbitrary = arbitraryBoundedEnum+  shrink = shrinkBoundedEnum++instance Arbitrary Digit1289 where+  arbitrary = arbitraryBoundedEnum+  shrink = shrinkBoundedEnum++instance Arbitrary Gender where+  arbitrary = arbitraryBoundedEnum+  shrink = shrinkBoundedEnum++instance Arbitrary Letter where+  arbitrary = arbitraryBoundedEnum+  shrink = shrinkBoundedEnum++instance Arbitrary ID where+  arbitrary = idFromTuple <$> arbitrary+  shrink = shrinkMap idFromTuple idToTuple++instance Arbitrary Location where+  arbitrary = arbitraryBoundedEnum+  shrink = shrinkBoundedEnum++instance Arbitrary Nationality where+  arbitrary = arbitraryBoundedEnum+  shrink = shrinkBoundedEnum++main :: IO ()+main = hspec $ do++  describe "Class laws" $ do++    testLawsMany @Digit+        [ boundedEnumLaws+        , eqLaws+        , numLaws+        , ordLaws+        , showLaws+        , showReadLaws+        ]++    testLawsMany @Gender+        [ boundedEnumLaws+        , eqLaws+        , ordLaws+        , showLaws+        , showReadLaws+        ]++    testLawsMany @ID+        [ eqLaws+        , ordLaws+        , showLaws+        , showReadLaws+        ]++    testLawsMany @Location+        [ boundedEnumLaws+        , eqLaws+        , ordLaws+        , showLaws+        , showReadLaws+        ]++    testLawsMany @Nationality+        [ boundedEnumLaws+        , eqLaws+        , ordLaws+        , showLaws+        , 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" $+      forAll (elements knownValidIDs) $ \i ->+        ID.fromText (ID.toText i) `shouldBe` Right i++    it "successfully parses valid identification numbers" $+      property $ \(i :: ID) ->+        ID.fromText (ID.toText i) `shouldBe` Right i++    it "does not parse identification numbers that are too short" $+      property $ \(i :: ID) n -> do+        let newLength = n `mod` 10+        let invalidID = T.take newLength $ ID.toText i+        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.InvalidLength++    it "does not parse identification numbers with invalid location codes" $+      property $ \(i :: ID) (c :: Int) -> do+        let invalidLocationCode = intToDigit $ c `mod` 10+        let invalidID = replaceCharAt 0 invalidLocationCode $ ID.toText i+        ID.fromText invalidID `shouldBe`+          Left (ID.InvalidChar 0 (CharRange 'A' 'Z'))++    it "does not parse identification numbers with invalid initial digits" $+      property $ \(i :: ID) ->+        forAll (elements ['0', '3', '4', '5', '6', '7']) $ \initialDigit -> do+          let invalidID = replaceCharAt 1 initialDigit (ID.toText i)+          let expectedError =+                ID.InvalidChar 1+                  (CharSet $ NESet.fromList $ '1' :| ['2', '8', '9'])+          ID.fromText invalidID `shouldBe` Left expectedError++    it "does not parse identification numbers with invalid checksums" $+      property $ \(i :: ID) (c :: Int) -> do+        let invalidChecksumDigit = intToDigit $+              ((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++    it "reports invalid characters even when input is too short" $+      property $ \(i :: ID) ->+      forAll (choose (1, 9)) $ \truncatedLength ->+      forAll (choose (0, truncatedLength - 1)) $ \invalidCharIndex -> do+        let textTruncated = T.take truncatedLength (ID.toText i)+        let textInvalid = replaceCharAt invalidCharIndex 'x' textTruncated+        ID.fromText textInvalid `shouldSatisfy` \case+          Left (ID.InvalidChar (CharIndex index) _)+            | index == invalidCharIndex -> True+          _ -> False++    it "does not report invalid characters if input is too long" $+      property $ \(i :: ID) (NonEmpty trailingExcess) ->+      forAll (choose (0, 9)) $ \invalidCharIndex -> do+        let textInvalid =+              replaceCharAt invalidCharIndex 'x' (ID.toText i)+              <>+              T.pack trailingExcess+        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.+--+replaceCharAt :: Int -> Char -> Text -> Text+replaceCharAt i c t+    | i < 0 || i >= T.length t = error "replaceCharAt: invalid index"+    | otherwise = prefix <> T.singleton c <> suffix+  where+    (prefix, suffix) = second (T.drop 1) (T.splitAt i t)++-- | A set of known-valid ID numbers.+--+-- Generated with 身分證字號產生器.+--+-- See: https://www.csie.ntu.edu.tw/~b90057/use/ROCid.html+--+knownValidIDs :: [ID]+knownValidIDs =+  [ ID.fromSymbol @"A123961383"+  , ID.fromSymbol @"B210742224"+  , ID.fromSymbol @"C120930548"+  , ID.fromSymbol @"D257991149"+  , ID.fromSymbol @"E127379116"+  , ID.fromSymbol @"F235628112"+  , ID.fromSymbol @"G105851924"+  , ID.fromSymbol @"H247910878"+  , ID.fromSymbol @"I118949082"+  , ID.fromSymbol @"J218475156"+  , ID.fromSymbol @"K150252170"+  , ID.fromSymbol @"L298479266"+  , ID.fromSymbol @"M114415878"+  , ID.fromSymbol @"N242846162"+  , ID.fromSymbol @"O184333688"+  , ID.fromSymbol @"P257366789"+  , ID.fromSymbol @"Q163999855"+  , ID.fromSymbol @"R275744925"+  , ID.fromSymbol @"S158047168"+  , ID.fromSymbol @"T296696104"+  , ID.fromSymbol @"U108929984"+  , ID.fromSymbol @"V245356279"+  , ID.fromSymbol @"W127612989"+  , ID.fromSymbol @"X234128072"+  , ID.fromSymbol @"Y140531128"+  , ID.fromSymbol @"Z250358466"+  ]++idFromTuple :: Digit ~ d => (Letter, Digit1289, d, d, d, d, d, d, d) -> ID+idFromTuple (x0, x1, x2, x3, x4, x5, x6, x7, x8) =+  ID x0 x1 x2 x3 x4 x5 x6 x7 x8++idToTuple :: Digit ~ d => ID -> (Letter, Digit1289, d, d, d, d, d, d, d)+idToTuple (ID x0 x1 x2 x3 x4 x5 x6 x7 x8) =+  (x0, x1, x2, x3, x4, x5, x6, x7, x8)
+ components/taiwan-id-test/Test/QuickCheck/Classes/Hspec.hs view
@@ -0,0 +1,72 @@+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}++-- | Provides testing functions to check that type class instances obey laws.+module Test.QuickCheck.Classes.Hspec+    ( testLaws+    , testLawsMany+    ) where++import Prelude++import Control.Monad+    ( forM_+    )+import Data.Proxy+    ( Proxy (..)+    )+import Data.Typeable+    ( Typeable+    , typeRep+    )+import Test.Hspec+    ( Spec+    , describe+    , it+    , parallel+    )+import Test.QuickCheck.Classes+    ( Laws (..)+    )++-- | Constructs a test to check that the given type class instance obeys the+--   given set of laws.+--+-- Example usage:+--+-- >>> testLaws @Natural ordLaws+-- >>> testLaws @(Map Int) functorLaws+testLaws+    :: forall a+     . Typeable a+    => (Proxy a -> Laws)+    -> Spec+testLaws getLaws =+    parallel+        $ describe description+        $ forM_ (lawsProperties laws)+        $ uncurry it+    where+        description =+            mconcat+                [ "Testing "+                , lawsTypeclass laws+                , " laws for type "+                , show (typeRep $ Proxy @a)+                ]+        laws = getLaws $ Proxy @a++-- | Calls `testLaws` with multiple sets of laws.+--+-- Example usage:+--+-- >>> testLawsMany @Natural [eqLaws, ordLaws]+-- >>> testLawsMany @(Map Int) [foldableLaws, functorLaws]+testLawsMany+    :: forall a+     . Typeable a+    => [Proxy a -> Laws]+    -> Spec+testLawsMany getLawsMany =+    testLaws @a `mapM_` getLawsMany
+ components/taiwan-id/Taiwan/ID.hs view
@@ -0,0 +1,366 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}++module Taiwan.ID+  (+  -- * Type+    ID (..)++  -- * Construction+  , fromSymbol+  , fromText+  , FromTextError (..)++  -- * Conversion+  , toText++  -- * Validity+  , checksum++  -- * Generation+  , generate++  -- * Inspection+  , getGender+  , getLocation+  , getNationality++  -- * Modification+  , setGender+  , setLocation+  , setNationality+  )+  where++import Control.Monad.Random.Class+  ( 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 Taiwan.ID.CharIndex+  ( CharIndex (..) )+import Taiwan.ID.CharSet+  ( CharSet (..) )+import Taiwan.ID.Digit+  ( Digit (..) )+import Taiwan.ID.Digit1289+  ( Digit1289 (..) )+import Taiwan.ID.Gender+  ( Gender (..) )+import Taiwan.ID.Letter+  ( Letter (..) )+import Taiwan.ID.Location+  ( Location )+import Taiwan.ID.Nationality+  ( Nationality (..) )+import Taiwan.ID.Unchecked+  ( UncheckedID (UncheckedID), ValidID )+import Taiwan.ID.Utilities+  ( guard, randomFinitary )+import Text.Read+  ( Lexeme (Ident, Symbol, Punc), Read (readPrec), lexP, parens, prec )++import qualified Data.Text as T+import qualified Taiwan.ID.Location as Location+import qualified Taiwan.ID.Unchecked as U++-- |+-- $setup+-- >>> :set -XDataKinds+-- >>> :set -XOverloadedStrings+-- >>> :set -XTypeApplications+-- >>> import Taiwan.ID+-- >>> import qualified Taiwan.ID as ID++--------------------------------------------------------------------------------+-- Type+--------------------------------------------------------------------------------++-- | Represents a __valid__ 10-digit uniform identification number of the form+-- __@A123456789@__.+--+-- By construction, invalid identification numbers are __not representable__ by+-- this data type.+--+-- 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 'checksum'.+--+data ID = ID+  { c0 :: !Letter+  , c1 :: !Digit1289+  , c2 :: !Digit+  , c3 :: !Digit+  , c4 :: !Digit+  , c5 :: !Digit+  , c6 :: !Digit+  , c7 :: !Digit+  , c8 :: !Digit+  }+  deriving stock (Eq, Ord, Generic)+  deriving anyclass Finitary++instance Read ID where+  readPrec = parens $ prec 10 $ do+    Ident  "ID"         <- lexP+    Symbol "."          <- lexP+    Ident  "fromSymbol" <- lexP+    Punc   "@"          <- lexP+    unsafeFromText <$> readPrec++instance Show ID where+  showsPrec d s =+    showParen (d > 10) $+      showString "ID.fromSymbol @" . shows (toText s)++--------------------------------------------------------------------------------+-- Construction+--------------------------------------------------------------------------------++-- | Constructs an 'ID' from a type-level textual symbol.+--+-- The symbol must be exactly 10 characters in length and of the form+-- __@A123456789@__:+--+-- >>> ID.fromSymbol @"A123456789"+-- ID.fromSymbol @"A123456789"+--+-- More precisely:+--+--  - the symbol must match the regular expression __@^[A-Z][1289][0-9]{8}$@__+--  - the resultant ID must have a valid checksum.+--+-- Failure to satisfy these constraints will result in one of the following+-- __type errors__:+--+-- === Invalid lengths+--+-- >>> ID.fromSymbol @"A12345678"+-- ...+-- ... An ID must have exactly 10 characters.+-- ...+--+-- === Invalid checksums+--+-- >>> ID.fromSymbol @"A123456780"+-- ...+-- ... ID has invalid checksum.+-- ...+--+-- === Invalid characters+--+-- On detection of an invalid character, the resulting type error reports+-- both the position of the character and the set of characters permitted+-- at that position.+--+-- >>> ID.fromSymbol @"_123456789"+-- ...+--     • "_123456789"+--        ^+--       Character at this position must be an uppercase letter.+-- ...+--+-- >>> ID.fromSymbol @"A_23456789"+-- ...+--     • "A_23456789"+--         ^+--       Character at this position must be a digit from the set {1, 2, 8, 9}.+-- ...+--+-- >>> ID.fromSymbol @"A1_3456789"+-- ...+--     • "A1_3456789"+--          ^+--       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@__:+--+-- >>> 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.+--+-- This function satisfies the following law:+--+-- @+-- 'fromText' ('toText' i) '==' 'Right' i+-- @+--+fromText :: Text -> Either FromTextError ID+fromText text = do+    unchecked <- first fromUncheckedError $ U.fromText text+    guard InvalidChecksum $ fromUnchecked unchecked+  where+    fromUncheckedError :: U.FromTextError -> FromTextError+    fromUncheckedError = \case+      U.InvalidChar i r ->+        InvalidChar i r+      U.InvalidLength ->+        InvalidLength++unsafeFromText :: Text -> ID+unsafeFromText t =+  case fromText t of+    Left _ -> error "unsafeFromText"+    Right i -> i++-- | Indicates an error that occurred while constructing an 'ID' from 'Text'.+--+data FromTextError++  = InvalidChar CharIndex CharSet+  -- ^ Indicates that the input text contains a character that is not allowed.+  --+  --   - `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.++  | InvalidLength+  -- ^ Indicates that the input text has an invalid length.++  deriving stock (Eq, Ord, Show)++--------------------------------------------------------------------------------+-- Conversion+--------------------------------------------------------------------------------++-- | Converts an 'ID' to 'Text'.+--+-- The output is of the form __@A123456789@__.+--+-- This function satisfies the following law:+--+-- @+-- 'fromText' ('toText' i) '==' 'Right' i+-- @+--+toText :: ID -> Text+toText = U.toText . toUnchecked++--------------------------------------------------------------------------------+-- Validity+--------------------------------------------------------------------------------++-- | Computes the terminal checksum digit of an 'ID'.+--+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)++--------------------------------------------------------------------------------+-- Generation+--------------------------------------------------------------------------------++-- | Generates a random 'ID'.+--+generate :: MonadRandom m => m ID+generate = randomFinitary++--------------------------------------------------------------------------------+-- Inspection+--------------------------------------------------------------------------------++-- | Decodes the 'Gender' component of an 'ID'.+--+getGender :: ID -> Gender+getGender ID {c1} = fst $ decodeC1 c1++-- | Decodes the 'Location' component of an 'ID'.+--+getLocation :: ID -> Location+getLocation ID {c0} = Location.fromLetter c0++-- | Decodes the 'Nationality' component of an 'ID'.+--+getNationality :: ID -> Nationality+getNationality ID {c1} = snd $ decodeC1 c1++--------------------------------------------------------------------------------+-- Modification+--------------------------------------------------------------------------------++-- | Updates the 'Gender' component of an 'ID'.+--+setGender :: Gender -> ID -> ID+setGender gender i = i {c1 = encodeC1 (gender, getNationality i)}++-- | Updates the 'Location' component of an 'ID'.+--+setLocation :: Location -> ID -> ID+setLocation location i = i {c0 = Location.toLetter location}++-- | Updates the 'Nationality' component of an 'ID'.+--+setNationality :: Nationality -> ID -> ID+setNationality nationality i = i {c1 = encodeC1 (getGender i, nationality)}++--------------------------------------------------------------------------------+-- Internal+--------------------------------------------------------------------------------++decodeC1 :: Digit1289 -> (Gender, Nationality)+decodeC1 = \case+  D1289_1 -> (  Male,    National)+  D1289_2 -> (Female,    National)+  D1289_8 -> (  Male, NonNational)+  D1289_9 -> (Female, NonNational)++encodeC1 :: (Gender, Nationality) -> Digit1289+encodeC1 = \case+  (  Male,    National) -> D1289_1+  (Female,    National) -> D1289_2+  (  Male, NonNational) -> D1289_8+  (Female, NonNational) -> D1289_9++fromUnchecked :: UncheckedID -> Maybe ID+fromUnchecked u@(UncheckedID u0 u1 u2 u3 u4 u5 u6 u7 u8 _) =+    case U.checksumValidity u of+      U.ChecksumValid   -> Just i+      U.ChecksumInvalid -> Nothing+  where+    i = ID u0 u1 u2 u3 u4 u5 u6 u7 u8++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 (checksum i)
+ components/taiwan-id/Taiwan/ID/CharIndex.hs view
@@ -0,0 +1,13 @@+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++module Taiwan.ID.CharIndex+  ( CharIndex (..)+  )+  where++-- | Specifies the zero-based position of a character within a string.+--+newtype CharIndex = CharIndex Int+  deriving stock (Read, Show)+  deriving newtype (Enum, Eq, Num, Ord)
+ components/taiwan-id/Taiwan/ID/CharSet.hs view
@@ -0,0 +1,18 @@+{-# LANGUAGE DerivingStrategies #-}++module Taiwan.ID.CharSet+  ( CharSet (..)+  )+  where++import Data.Set.NonEmpty+  ( NESet )++-- | Specifies a set of characters.+--+data CharSet+  = CharSet (NESet Char)+  -- ^ An explicit set of characters.+  | CharRange Char Char+  -- ^ An inclusive range of characters.+  deriving stock (Eq, Ord, Read, Show)
+ components/taiwan-id/Taiwan/ID/Digit.hs view
@@ -0,0 +1,119 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++module Taiwan.ID.Digit+  ( Digit (..)+  , fromChar+  , toChar+  , generate+  , FromChar+  , FromNat+  , ToNat+  ) where++import Control.Monad.Random+  ( MonadRandom )+import Data.Finitary+  ( Finitary )+import GHC.Generics+  ( Generic )+import GHC.TypeNats+  ( Nat )+import Taiwan.ID.Utilities+  ( maybeFinitary, randomFinitary )+import Text.Read+  ( Read (readPrec), readMaybe )++import Prelude hiding+  ( fromIntegral )++import qualified Prelude++-- | Represents a single decimal digit in the range @0@ to @9@.+--+data Digit+  = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9+  deriving stock (Bounded, Enum, Eq, Generic, Ord)+  deriving anyclass Finitary++-- | Arithmetic modulo 10.+--+instance Num Digit where+  a + b = fromIntegral (fromEnum a + fromEnum b)+  a * b = fromIntegral (fromEnum a * fromEnum b)+  a - b = fromIntegral (fromEnum a - fromEnum b)+  abs a = a+  fromInteger = fromIntegral+  signum D0 = D0+  signum __ = D1++instance Read Digit where readPrec = fromInteger <$> readPrec++instance Show Digit where show = show . fromEnum++-- | Attempts to parse a 'Digit' from a character.+--+-- The 'Char' must be a decimal digit in the range @0@ to @9@.+--+fromChar :: Char -> Maybe Digit+fromChar c = readMaybe [c] >>= maybeFinitary++-- | Converts a 'Digit' to a decimal digit character.+--+toChar :: Digit -> Char+toChar digit = case show digit of+  [c] -> c+  _ -> error "toChar"++-- | Creates a 'Digit' from an integral number (modulo 10).+--+fromIntegral :: Integral i => i -> Digit+fromIntegral i = toEnum (Prelude.fromIntegral (i `mod` 10))++-- | Generates a random digit.+--+generate :: MonadRandom m => m Digit+generate = randomFinitary++type family FromChar (c :: Char) :: Maybe Digit where+  FromChar '0' = Just D0+  FromChar '1' = Just D1+  FromChar '2' = Just D2+  FromChar '3' = Just D3+  FromChar '4' = Just D4+  FromChar '5' = Just D5+  FromChar '6' = Just D6+  FromChar '7' = Just D7+  FromChar '8' = Just D8+  FromChar '9' = Just D9+  FromChar _   = Nothing++type family FromNat (n :: Nat) :: Maybe Digit where+  FromNat 0 = Just D0+  FromNat 1 = Just D1+  FromNat 2 = Just D2+  FromNat 3 = Just D3+  FromNat 4 = Just D4+  FromNat 5 = Just D5+  FromNat 6 = Just D6+  FromNat 7 = Just D7+  FromNat 8 = Just D8+  FromNat 9 = Just D9+  FromNat _ = Nothing++type family ToNat (d :: Digit) :: Nat where+  ToNat D0 = 0+  ToNat D1 = 1+  ToNat D2 = 2+  ToNat D3 = 3+  ToNat D4 = 4+  ToNat D5 = 5+  ToNat D6 = 6+  ToNat D7 = 7+  ToNat D8 = 8+  ToNat D9 = 9
+ components/taiwan-id/Taiwan/ID/Digit1289.hs view
@@ -0,0 +1,94 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++module Taiwan.ID.Digit1289+  ( Digit1289 (..)+  , fromChar+  , toChar+  , toDigit+  , generate+  , FromChar+  , FromNat+  , ToNat+  ) where++import Control.Monad.Random+  ( MonadRandom )+import Data.Finitary+  ( Finitary )+import GHC.Generics+  ( Generic )+import GHC.TypeNats+  ( Nat )+import Taiwan.ID.Digit+  ( Digit (..) )+import Taiwan.ID.Utilities+  ( randomFinitary )++-- | Represents a single decimal digit from the set {@1@, @2@, @8@, @9@}.+--+data Digit1289+  = D1289_1 | D1289_2 | D1289_8 | D1289_9+  deriving stock (Bounded, Enum, Eq, Generic, Ord, Read, Show)+  deriving anyclass Finitary++-- | Attempts to parse a 'Digit1289' from a character.+--+-- Only the characters @'1'@, @'2'@, @'8'@, and @'9'@ are accepted.+--+fromChar :: Char -> Maybe Digit1289+fromChar = \case+  '1' -> Just D1289_1+  '2' -> Just D1289_2+  '8' -> Just D1289_8+  '9' -> Just D1289_9+  _   -> Nothing++-- | Converts a 'Digit1289' to a decimal digit character.+--+toChar :: Digit1289 -> Char+toChar = \case+  D1289_1 -> '1'+  D1289_2 -> '2'+  D1289_8 -> '8'+  D1289_9 -> '9'++-- | Converts a 'Digit1289' to an ordinary 'Digit'.+--+toDigit :: Digit1289 -> Digit+toDigit = \case+  D1289_1 -> D1+  D1289_2 -> D2+  D1289_8 -> D8+  D1289_9 -> D9++-- | Generates a random 'Digit1289'.+--+generate :: MonadRandom m => m Digit1289+generate = randomFinitary++type family FromChar (c :: Char) :: Maybe Digit1289 where+  FromChar '1' = Just D1289_1+  FromChar '2' = Just D1289_2+  FromChar '8' = Just D1289_8+  FromChar '9' = Just D1289_9+  FromChar _   = Nothing++type family FromNat (n :: Nat) :: Maybe Digit1289 where+  FromNat 1 = Just D1289_1+  FromNat 2 = Just D1289_2+  FromNat 8 = Just D1289_8+  FromNat 9 = Just D1289_9+  FromNat _ = Nothing++type family ToNat (d :: Digit1289) :: Nat where+  ToNat D1289_1 = 1+  ToNat D1289_2 = 2+  ToNat D1289_8 = 8+  ToNat D1289_9 = 9
+ components/taiwan-id/Taiwan/ID/Gender.hs view
@@ -0,0 +1,52 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}++module Taiwan.ID.Gender+  ( Gender (..)+  , toText+  , generate+  ) where++import Control.Monad.Random.Class+  ( MonadRandom (..) )+import Data.Finitary+  ( Finitary )+import Data.Text+  ( Text )+import GHC.Generics+  ( Generic )+import Taiwan.ID.Language+  ( Language (..) )+import Taiwan.ID.Utilities+  ( randomFinitary )++-- | A person's gender.+--+data Gender = Male | Female+  deriving stock (Bounded, Enum, Eq, Generic, Ord, Read, Show)+  deriving anyclass Finitary++-- | Prints the specified 'Gender'.+--+toText :: Language -> Gender -> Text+toText = \case+  English -> toTextEnglish+  Chinese -> toTextChinese++toTextEnglish :: Gender -> Text+toTextEnglish = \case+  Male   -> "Male"+  Female -> "Female"++toTextChinese :: Gender -> Text+toTextChinese = \case+  Male   -> "男性"+  Female -> "女性"++-- | Generates a random 'Gender'.+--+generate :: MonadRandom m => m Gender+generate = randomFinitary
+ components/taiwan-id/Taiwan/ID/Language.hs view
@@ -0,0 +1,5 @@+module Taiwan.ID.Language where++-- | A language into which values can be localized when pretty printing.+--+data Language = English | Chinese
+ components/taiwan-id/Taiwan/ID/Letter.hs view
@@ -0,0 +1,69 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++module Taiwan.ID.Letter+  ( Letter (..)+  , fromChar+  , toChar+  , generate+  , FromChar+  ) where++import Control.Monad.Random.Class+  ( MonadRandom (..) )+import Data.Finitary+  ( Finitary )+import GHC.Generics+  ( Generic )+import Taiwan.ID.Utilities+  ( randomFinitary )+import Text.Read+  ( readMaybe )++-- | Represents a letter in the latin alphabet.+--+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 stock (Bounded, Enum, Eq, Generic, Ord, Read, Show)+  deriving anyclass Finitary++-- | Attempts to parse a 'Letter' from a character.+--+-- Returns 'Nothing' if the specified character is not an uppercase alphabetic+-- character.+--+fromChar :: Char -> Maybe Letter+fromChar c = readMaybe [c]++-- | Converts the specified 'Letter' to a character.+--+toChar :: Letter -> Char+toChar letter = case show letter of+  [c] -> c+  _ -> error "toChar"++-- | Generates a random 'Letter'.+--+generate :: MonadRandom m => m Letter+generate = randomFinitary++type family FromChar (c :: Char) :: Maybe Letter where+  FromChar 'A' = Just A; FromChar 'N' = Just N+  FromChar 'B' = Just B; FromChar 'O' = Just O+  FromChar 'C' = Just C; FromChar 'P' = Just P+  FromChar 'D' = Just D; FromChar 'Q' = Just Q+  FromChar 'E' = Just E; FromChar 'R' = Just R+  FromChar 'F' = Just F; FromChar 'S' = Just S+  FromChar 'G' = Just G; FromChar 'T' = Just T+  FromChar 'H' = Just H; FromChar 'U' = Just U+  FromChar 'I' = Just I; FromChar 'V' = Just V+  FromChar 'J' = Just J; FromChar 'W' = Just W+  FromChar 'K' = Just K; FromChar 'X' = Just X+  FromChar 'L' = Just L; FromChar 'Y' = Just Y+  FromChar 'M' = Just M; FromChar 'Z' = Just Z+  FromChar _ = Nothing
+ components/taiwan-id/Taiwan/ID/Location.hs view
@@ -0,0 +1,197 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-}++module Taiwan.ID.Location+  ( Location+  , fromLetter+  , toLetter+  , toText+  , generate+  ) where++import Control.Monad.Random.Class+  ( MonadRandom (..) )+import Data.Finitary+  ( Finitary )+import Data.Text+  ( Text )+import GHC.Generics+  ( Generic )+import Taiwan.ID.Language+  ( Language (..) )+import Taiwan.ID.Letter+  ( Letter (..) )+import Taiwan.ID.Utilities+  ( randomFinitary )+import Text.Read+  ( Lexeme (Ident, Symbol), Read (readPrec), lexP, parens )++-- | Represents a geographical location.+--+-- == Location codes+--+-- Every location has a unique letter code:+--+-- +------+---------+-------------------++-- | Code | Chinese | English           |+-- +======+=========+===================++-- | @A@  | 臺北市     | Taipei City       |+-- +------+---------+-------------------++-- | @B@  | 臺中市     | Taichung City     |+-- +------+---------+-------------------++-- | @C@  | 基隆市     | Keelung City      |+-- +------+---------+-------------------++-- | @D@  | 臺南市     | Tainan City       |+-- +------+---------+-------------------++-- | @E@  | 高雄市     | Kaohsiung City    |+-- +------+---------+-------------------++-- | @F@  | 新北市     | New Taipei City   |+-- +------+---------+-------------------++-- | @G@  | 宜蘭縣     | Yilan County      |+-- +------+---------+-------------------++-- | @H@  | 桃園市     | Taoyuan City      |+-- +------+---------+-------------------++-- | @I@  | 嘉義市     | Chiayi City       |+-- +------+---------+-------------------++-- | @J@  | 新竹縣     | Hsinchu County    |+-- +------+---------+-------------------++-- | @K@  | 苗栗縣     | Miaoli County     |+-- +------+---------+-------------------++-- | @L@  | 臺中縣     | Taichung County   |+-- +------+---------+-------------------++-- | @M@  | 南投縣     | Nantou County     |+-- +------+---------+-------------------++-- | @N@  | 彰化縣     | Changhua County   |+-- +------+---------+-------------------++-- | @O@  | 新竹市     | Hsinchu City      |+-- +------+---------+-------------------++-- | @P@  | 雲林縣     | Yunlin County     |+-- +------+---------+-------------------++-- | @Q@  | 嘉義縣     | Chiayi County     |+-- +------+---------+-------------------++-- | @R@  | 臺南縣     | Tainan County     |+-- +------+---------+-------------------++-- | @S@  | 高雄縣     | Kaohsiung County  |+-- +------+---------+-------------------++-- | @T@  | 屏東縣     | Pingtung County   |+-- +------+---------+-------------------++-- | @U@  | 花蓮縣     | Hualien County    |+-- +------+---------+-------------------++-- | @V@  | 臺東縣     | Taitung County    |+-- +------+---------+-------------------++-- | @W@  | 金門縣     | Kinmen County     |+-- +------+---------+-------------------++-- | @X@  | 澎湖縣     | Penghu County     |+-- +------+---------+-------------------++-- | @Y@  | 陽明山     | Yangmingshan      |+-- +------+---------+-------------------++-- | @Z@  | 連江縣     | Lienchiang County |+-- +------+---------+-------------------++--+-- == Usage+--+-- To construct a 'Location' from its letter code, use the 'fromLetter'+-- function.+--+-- To print the full name of a 'Location', use the 'toText' function.+--+-- To generate a random 'Location', use the 'generate' function.+--+newtype Location = Location Letter+  deriving stock (Eq, Generic, Ord)+  deriving newtype (Bounded, Enum)+  deriving anyclass Finitary++instance Read Location where+  readPrec = parens $ do+    Ident "Location"   <- lexP+    Symbol "."         <- lexP+    Ident "fromLetter" <- lexP+    fromLetter <$> readPrec++instance Show Location where+  showsPrec _ s =+    showString "Location.fromLetter " . shows (toLetter s)++-- | Constructs a 'Location' from its corresponding letter code.+--+fromLetter :: Letter -> Location+fromLetter = Location++-- | Converts a 'Location' to its corresponding letter code.+--+toLetter :: Location -> Letter+toLetter (Location letter) = letter++-- | Prints the specified 'Location'.+toText :: Language -> Location -> Text+toText = \case+  English -> toTextEnglish+  Chinese -> toTextChinese++toTextChinese :: Location -> Text+toTextChinese (Location letter) = case letter of+  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 -> "連江縣"++toTextEnglish :: Location -> Text+toTextEnglish (Location letter) = case letter of+  A -> "Taipei City"+  B -> "Taichung City"+  C -> "Keelung City"+  D -> "Tainan City"+  E -> "Kaohsiung City"+  F -> "New Taipei City"+  G -> "Yilan County"+  H -> "Taoyuan City"+  I -> "Chiayi City"+  J -> "Hsinchu County"+  K -> "Miaoli County"+  L -> "Taichung County"+  M -> "Nantou County"+  N -> "Changhua County"+  O -> "Hsinchu City"+  P -> "Yunlin County"+  Q -> "Chiayi County"+  R -> "Tainan County"+  S -> "Kaohsiung County"+  T -> "Pingtung County"+  U -> "Hualien County"+  V -> "Taitung County"+  W -> "Kinmen County"+  X -> "Penghu County"+  Y -> "Yangmingshan"+  Z -> "Lienchiang County"++-- | Generates a random 'Location'.+--+generate :: MonadRandom m => m Location+generate = randomFinitary
+ components/taiwan-id/Taiwan/ID/Nationality.hs view
@@ -0,0 +1,29 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingStrategies #-}++module Taiwan.ID.Nationality+  ( Nationality (..)+  , generate+  )+  where++import Control.Monad.Random.Class+  ( MonadRandom (..) )+import Data.Finitary+  ( Finitary )+import GHC.Generics+  ( Generic )+import Taiwan.ID.Utilities+  ( randomFinitary )++-- | Specifies a person's nationality.+--+data Nationality = National | NonNational+  deriving stock (Bounded, Enum, Eq, Ord, Generic, Read, Show)+  deriving anyclass Finitary++-- | Generates a random 'Nationality'.+--+generate :: MonadRandom m => m Nationality+generate = randomFinitary
+ components/taiwan-id/Taiwan/ID/Unchecked.hs view
@@ -0,0 +1,315 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}++module Taiwan.ID.Unchecked+  ( UncheckedID (..)+  , UncheckedIDTuple+  , FromTextError (..)+  , fromText+  , toText+  , checksum+  , checksumValidity+  , ChecksumValidity (..)+  , ValidID+  )+  where++import Control.Monad+  ( when )+import Data.Kind+  ( Constraint )+import Data.List.NonEmpty+  ( NonEmpty ((:|)) )+import Data.Text+  ( Text )+import Data.Type.Bool+  ( If )+import Data.Type.Equality+  ( type (==) )+import GHC.TypeError+  ( Assert, TypeError )+import GHC.TypeLits+  ( AppendSymbol, KnownSymbol, Symbol )+import GHC.TypeNats+  ( CmpNat, Mod, Nat, type (+) )+import Taiwan.ID.CharIndex+  ( CharIndex (..) )+import Taiwan.ID.CharSet+  ( CharSet (..) )+import Taiwan.ID.Digit+  ( Digit (..) )+import Taiwan.ID.Digit1289+  ( Digit1289 (..) )+import Taiwan.ID.Letter+  ( Letter (..) )+import Taiwan.ID.Utilities+  ( FromJust, Fst, ReplicateChar, Snd, SymbolLength, SymbolToCharList, guard )++import qualified Data.Set.NonEmpty as NESet+import qualified Data.Text as T+import qualified GHC.TypeError as TypeError+import qualified GHC.TypeNats as N+import qualified Taiwan.ID.Digit as Digit+import qualified Taiwan.ID.Digit1289 as Digit1289+import qualified Taiwan.ID.Letter as Letter++data UncheckedID = UncheckedID+  { c0 :: !Letter+  , c1 :: !Digit1289+  , c2 :: !Digit+  , c3 :: !Digit+  , c4 :: !Digit+  , c5 :: !Digit+  , c6 :: !Digit+  , c7 :: !Digit+  , c8 :: !Digit+  , c9 :: !Digit+  }+  deriving stock (Eq, Ord, Show)++type UncheckedIDTuple =+  ( Letter+  , Digit1289+  , Digit+  , Digit+  , Digit+  , Digit+  , Digit+  , Digit+  , Digit+  , Digit+  )++data FromTextError+  = 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 InvalidLength+    (text1,  c0                             ) <- parseLetter    text0+    (text2,  c1                             ) <- parseDigit1289 text1+    (_____, (c2, c3, c4, c5, c6, c7, c8, c9)) <- parseDigits    text2+    pure UncheckedID {c0, c1, c2, c3, c4, c5, c6, c7, c8, c9}+  where+    parseLetter :: Parser Letter+    parseLetter text = do+      (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 InvalidLength $ T.uncons text+      digit1289 <- guard+        (InvalidChar 1 (CharSet $ NESet.fromList $ '1' :| ['2', '8', '9']))+        (Digit1289.fromChar char)+      pure (remainder, digit1289)++    parseDigits :: d ~ Digit => Parser (d, d, d, d, d, d, d, d)+    parseDigits text = do+        let (chars, remainder) = T.splitAt 8 text+        digitList <- traverse parseIndexedDigit (zip [2 ..] $ T.unpack chars)+        digitTuple <- guard InvalidLength (listToTuple8 digitList)+        pure (remainder, digitTuple)+      where+        parseIndexedDigit (i, c) =+          guard (InvalidChar i (CharRange '0' '9')) (Digit.fromChar c)++toText :: UncheckedID -> Text+toText UncheckedID {c0, c1, c2, c3, c4, c5, c6, c7, c8, c9} =+  T.pack+    ( Letter.toChar c0+    : Digit1289.toChar c1+    : fmap Digit.toChar [c2, c3, c4, c5, c6, c7, c8, c9]+    )++checksum :: UncheckedID -> Digit+checksum (UncheckedID u0 (Digit1289.toDigit -> u1) u2 u3 u4 u5 u6 u7 u8 u9) =+  sum $ zipWith (*)+    [ 1,  9,  8,  7,  6,  5,  4,  3,  2,  1,  1]+    [a0, a1, u1, u2, u3, u4, u5, u6, u7, u8, u9]+  where+    (a0, a1) = checksumLetterToDigitPair u0++checksumLetterToDigitPair :: Letter -> (Digit, Digit)+checksumLetterToDigitPair = \case+  A -> (1, 0); N -> (2, 2)+  B -> (1, 1); O -> (3, 5)+  C -> (1, 2); P -> (2, 3)+  D -> (1, 3); Q -> (2, 4)+  E -> (1, 4); R -> (2, 5)+  F -> (1, 5); S -> (2, 6)+  G -> (1, 6); T -> (2, 7)+  H -> (1, 7); U -> (2, 8)+  I -> (3, 4); V -> (2, 9)+  J -> (1, 8); W -> (3, 2)+  K -> (1, 9); X -> (3, 0)+  L -> (2, 0); Y -> (3, 1)+  M -> (2, 1); Z -> (3, 3)++data ChecksumValidity+  = ChecksumValid+  | ChecksumInvalid+  deriving stock (Eq, Show)++checksumValidity :: UncheckedID -> ChecksumValidity+checksumValidity u =+  case checksum u of+    0 -> ChecksumValid+    _ -> ChecksumInvalid++listToTuple8 :: [a] -> Maybe (a, a, a, a, a, a, a, a)+listToTuple8 = \case+  (a0 : a1 : a2 : a3 : a4 : a5 : a6 : a7 : _) ->+    Just (a0, a1, a2, a3, a4, a5, a6, a7)+  _ ->+    Nothing++type family ChecksumValid (id :: UncheckedIDTuple) :: Constraint where+  ChecksumValid id =+    Assert+      (ChecksumDigit id == D0)+      (TypeError (TypeError.Text "ID has invalid checksum."))++type family ChecksumDigit (id :: UncheckedIDTuple) :: Digit where+  ChecksumDigit id = ChecksumDigitFromNat (Mod (Checksum id) 10)++type family ChecksumDigitFromNat (n :: Nat) :: Digit where+  ChecksumDigitFromNat n =+    FromJust+      (Digit.FromNat n)+      (TypeError (TypeError.Text "Expected natural number between 0 and 9."))++type family Checksum (id :: UncheckedIDTuple) :: Nat where+  Checksum '(c0, c1, c2, c3, c4, c5, c6, c7, c8, c9) =+    (     (ChecksumLetterToNat0 c0 N.* 1)+      N.+ (ChecksumLetterToNat1 c0 N.* 9)+      N.+ (Digit1289.ToNat      c1 N.* 8)+      N.+ (Digit.ToNat          c2 N.* 7)+      N.+ (Digit.ToNat          c3 N.* 6)+      N.+ (Digit.ToNat          c4 N.* 5)+      N.+ (Digit.ToNat          c5 N.* 4)+      N.+ (Digit.ToNat          c6 N.* 3)+      N.+ (Digit.ToNat          c7 N.* 2)+      N.+ (Digit.ToNat          c8 N.* 1)+      N.+ (Digit.ToNat          c9 N.* 1)+    )++type family ChecksumLetterToNat0 (letter :: Letter) :: Nat where+  ChecksumLetterToNat0 x = Fst (ChecksumLetterToNatPair x)++type family ChecksumLetterToNat1 (letter :: Letter) :: Nat where+  ChecksumLetterToNat1 x = Snd (ChecksumLetterToNatPair x)++type family ChecksumLetterToNatPair (l :: Letter) :: (Nat, Nat) where+  ChecksumLetterToNatPair A = '(1, 0); ChecksumLetterToNatPair B = '(1, 1)+  ChecksumLetterToNatPair C = '(1, 2); ChecksumLetterToNatPair D = '(1, 3)+  ChecksumLetterToNatPair E = '(1, 4); ChecksumLetterToNatPair F = '(1, 5)+  ChecksumLetterToNatPair G = '(1, 6); ChecksumLetterToNatPair H = '(1, 7)+  ChecksumLetterToNatPair I = '(3, 4); ChecksumLetterToNatPair J = '(1, 8)+  ChecksumLetterToNatPair K = '(1, 9); ChecksumLetterToNatPair L = '(2, 0)+  ChecksumLetterToNatPair M = '(2, 1); ChecksumLetterToNatPair N = '(2, 2)+  ChecksumLetterToNatPair O = '(3, 5); ChecksumLetterToNatPair P = '(2, 3)+  ChecksumLetterToNatPair Q = '(2, 4); ChecksumLetterToNatPair R = '(2, 5)+  ChecksumLetterToNatPair S = '(2, 6); ChecksumLetterToNatPair T = '(2, 7)+  ChecksumLetterToNatPair U = '(2, 8); ChecksumLetterToNatPair V = '(2, 9)+  ChecksumLetterToNatPair W = '(3, 2); ChecksumLetterToNatPair X = '(3, 0)+  ChecksumLetterToNatPair Y = '(3, 1); ChecksumLetterToNatPair Z = '(3, 3)++type family SymbolToId (s :: Symbol) :: UncheckedIDTuple where+  SymbolToId s =+    IdFromCharList s (SymbolToCharList s)++type family+    IdFromCharList (id :: Symbol) (xs :: [Char]) :: UncheckedIDTuple+  where+    IdFromCharList id '[c0, c1, c2, c3, c4, c5, c6, c7, c8, c9] =+      '( LetterFromChar    id 0 c0+       , Digit1289FromChar id 1 c1+       , DigitFromChar     id 2 c2+       , DigitFromChar     id 3 c3+       , DigitFromChar     id 4 c4+       , DigitFromChar     id 5 c5+       , DigitFromChar     id 6 c6+       , DigitFromChar     id 7 c7+       , DigitFromChar     id 8 c8+       , DigitFromChar     id 9 c9+       )+    IdFromCharList _ _ =+      TypeError (TypeError.Text "An ID must have exactly 10 characters.")++type family+    DigitFromChar (id :: Symbol) (index :: Nat) (c :: Char) :: Digit+  where+    DigitFromChar id index c =+      FromJust+        (Digit.FromChar c)+        (InvalidCharError id index DigitTypeError)++type family+    Digit1289FromChar (id :: Symbol) (index :: Nat) (c :: Char) :: Digit1289+  where+    Digit1289FromChar id index c =+      FromJust+        (Digit1289.FromChar c)+        (InvalidCharError id index Digit1289TypeError)++type family+    LetterFromChar (id :: Symbol) (index :: Nat) (c :: Char) :: Letter+  where+    LetterFromChar id index c =+      FromJust+        (Letter.FromChar c)+        (InvalidCharError id index LetterTypeError)++type DigitTypeError =+  "Character at this position must be a digit in the range [0 .. 9]."++type Digit1289TypeError =+  "Character at this position must be a digit from the set {1, 2, 8, 9}."++type LetterTypeError =+  "Character at this position must be an uppercase letter."++type family InvalidCharError+    (invalidId :: Symbol) (charIndex :: Nat) (message :: Symbol)+  where+    InvalidCharError invalidId charIndex message =+      TypeError+        ( TypeError.ShowType invalidId+          TypeError.:$$:+          TypeError.Text (ReplicateChar (charIndex + 1) ' ' `AppendSymbol` "^")+          TypeError.:$$:+          TypeError.Text message+        )++type ValidID s =+  ( KnownSymbol 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\"."
+ components/taiwan-id/Taiwan/ID/Utilities.hs view
@@ -0,0 +1,90 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++module Taiwan.ID.Utilities where++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, type (<=), type (+) )+import GHC.TypeNats+  ( 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++maybeFinitary :: forall a. Finitary a => Natural -> Maybe a+maybeFinitary = fmap fromFinite . packFinite . fromIntegral @Natural @Integer++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++type family Fst (t :: (a, a)) :: a where+  Fst '(x, _) = x++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]+  where+    SymbolToCharList s = MaybeCharSymbolToCharList (UnconsSymbol s)++type family+  MaybeCharSymbolToCharList+    (m :: Maybe (Char, Symbol)) :: [Char]+  where+    MaybeCharSymbolToCharList ('Just '(c, rest)) = c ': SymbolToCharList rest+    MaybeCharSymbolToCharList 'Nothing = '[]++type family ReplicateChar (n :: Nat) (c :: Char) :: Symbol where+  ReplicateChar n c = ReplicateChar' "" n c++type family ReplicateChar' (s :: Symbol) (n :: Nat) (c :: Char) :: Symbol where+  ReplicateChar' s 0 _ = s+  ReplicateChar' s n c = ReplicateChar' (ConsSymbol c s) (n - 1) c
+ taiwan-id.cabal view
@@ -0,0 +1,139 @@+cabal-version:  3.0+name:           taiwan-id+version:        0.0.0.0+synopsis:       Implementation of Taiwan's uniform ID number format.+category:       Identification+homepage:       https://github.com/jonathanknowles/taiwan-id#readme+bug-reports:    https://github.com/jonathanknowles/taiwan-id/issues+author:         Jonathan Knowles+maintainer:     mail@jonathanknowles.net+copyright:      Jonathan Knowles+license:        BSD-3-Clause+license-file:   LICENSE+build-type:     Custom++description:++  This package provides a Haskell implementation of Taiwan's uniform+  identification number format.++  This number format is used by both National Identification Cards (國民身分證)+  and Alien Resident Certificates (外僑居留證) issued by the Republic of China+  (ROC) government to individuals, with numbers assigned under each system+  occupying disjoint parts of the same identifier space.++  Each identification number consists of a single uppercase letter followed by+  nine decimal digits, with the final digit serving as a checksum calculated+  according to a standard algorithm.++  Example: `A123456789`++  This package offers functions for validating, decoding, and encoding these+  numbers.++  See the "Taiwan.ID" module to get started.++  For more details, see:++  * https://zh.wikipedia.org/wiki/中華民國國民身分證+  * https://en.wikipedia.org/wiki/National_identification_card_(Taiwan)+  * https://en.wikipedia.org/wiki/Resident_certificate++extra-doc-files:+  CHANGELOG.md+  README.md++common dependency-base+    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+    build-depends:nonempty-containers       >= 0.3.5.0      && < 0.4+common dependency-QuickCheck+    build-depends:QuickCheck                >= 2.13.2       && < 2.18+common dependency-quickcheck-classes+    build-depends:quickcheck-classes        >= 0.6.5.0      && < 0.7+common dependency-text+    build-depends:text                      >= 1.2.3.1      && < 2.2++custom-setup+  setup-depends:+    , base                                  >= 4.17.2.1     && < 4.22+    , cabal-doctest                         >= 1.0.12       && < 1.1++source-repository head+  type: git+  location: https://github.com/jonathanknowles/taiwan-id++library+  import:+    , dependency-base+    , dependency-finitary+    , dependency-finite-typelits+    , dependency-MonadRandom+    , dependency-nonempty-containers+    , dependency-text+  exposed-modules:+      Taiwan.ID+      Taiwan.ID.CharIndex+      Taiwan.ID.CharSet+      Taiwan.ID.Digit+      Taiwan.ID.Digit1289+      Taiwan.ID.Gender+      Taiwan.ID.Language+      Taiwan.ID.Letter+      Taiwan.ID.Location+      Taiwan.ID.Nationality+  other-modules:+      Taiwan.ID.Unchecked+      Taiwan.ID.Utilities+  hs-source-dirs:+      components/taiwan-id+  ghc-options: -Wall+  default-language: Haskell2010++test-suite taiwan-id-test+  import:+    , dependency-base+    , dependency-finitary+    , dependency-hspec+    , dependency-MonadRandom+    , dependency-microlens+    , dependency-nonempty-containers+    , dependency-QuickCheck+    , dependency-quickcheck-classes+    , dependency-text+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  other-modules:+      Test.QuickCheck.Classes.Hspec+  hs-source-dirs:+      components/taiwan-id-test+  ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N+  build-depends:+    , taiwan-id+  default-language: Haskell2010++test-suite taiwan-id-test-docs+  import:+    , dependency-base+    , dependency-doctest+  build-depends:+    , taiwan-id+  x-doctest-options: --verbose+  type: exitcode-stdio-1.0+  main-is: Main.hs+  hs-source-dirs:+    components/taiwan-id-test-docs+  ghc-options: -threaded+  default-language: Haskell2010