Represents a valid 10-digit ROC (Taiwan) 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.

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".
...

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

Indicates an error that occurred while constructing an ID from Text.

Converts an ID to Text.

The output is of the form A123456789.

This function satisfies the following law:

fromText (toText i) == Right i

Computes the terminal checksum digit of an ID.

Generates a random ID.

Decodes the Gender component of an ID.

Decodes the Location component of an ID.

Decodes the Nationality component of an ID.

Updates the Gender component of an ID.

Updates the Location component of an ID.

Updates the Nationality component of an ID.