The Avail Programming Language
Mobile Users: Click here to view our text rendering warning.


Type lattice: focus on character. any any ⊤--any nontype nontype any--nontype character character nontype--character ¢+ type {¢+}ᵀ character--¢+ type ¢3 type {¢3}ᵀ character--¢3 type ¢a type {¢a}ᵀ character--¢a type ¢A type {¢A}ᵀ character--¢A type …1 …1--¢+ type ¢+ type--¢3 type ¢+ type--⊥ ¢3 type--¢a type ¢3 type--⊥ ¢a type--¢A type ¢a type--⊥ …2 ¢A type--…2 ¢A type--⊥

A character is a sign or symbol in the semiotic sense: an entity with distinct identity that is nonetheless generally intended and understood to represent something other than itself. The visual representation of a character is a glyph. A character is necessarily distinct from how it is written or printed. The same character will differ in any two handwritten occurrences, even when the same person is responsible for the production of both. Likewise the printed representation of a character will differ by font or style. For example, each of "a", "a", and "a" are understood by readers of Roman-influenced languages as representing the same character. So a character has identity independent of any and all glyphs that transcribe it.

Avail is only concerned with character value, not meaning or transcription. A character is always equal to itself and always unequal to another character. Characters are immutable and possess but a single intrinsic property: Unicode code point. Unicode is an international standard for the codification of all widely used characters. A code point is a numeric value that is uniquely associated with a character relative to some system of codification. Thus a character's Unicode code point singularly identifies it within the Unicode scheme.

For each of "abcde" do [ c : character | /* A character and a code point are distinct in Avail. */ Assert: c ≠ c's code point; Assert: c = c's code point→character; ];

A character literal is expressed as a cent sign ¢ (U+00A2) followed by a single-character lexeme or length-one string literal. Avail character literal notation is provided by the method "¢…". The single-character form is sufficient for nearly every character, but the string literal form must be employed when the desired character is a quotation mark " (U+0022), semicolon ; (U+003B), or non-printable character.

Assert: "cat"[1] = ¢c; Assert: "dog"[2] = ¢o; Assert: "42"[1] = ¢4; /* The first character of the next string is a horizontal tab. */ Assert: " tab"[1] = ¢"\t";
nontype | Return to Type System | number