Fwd: The Char Kind: proposal

[Daniel Rogozin]

Greetings,


I would like to propose and discuss several changes related to the
character kind. Some of those changes were implemented jointly with Rinat
Stryungis, my Serokell teammate.

The purpose of this patch is to provide a possibility of analysing
type-level strings (symbols) as term-level ones. This feature allows users
to implement such programs as type-level parsers. One needs to have
full-fledged support of type-level characters as well as we already have
for strings and numbers. In addition to this functionality, it makes sense
to introduce the set of type-families, counterparts of functions defined in
the Data.Char module in order to work with type-level strings and chars as
usual (more or less).

For more convenience, it’s worth having some of the character-related type
families as built-ins and generating the rest of ones as type synonyms.

The patch fixes #11342, an issue opened by Alexander Vieth several years
ago. In this patch, we introduced the Char Kind, a kind of type-level
characters, with the additional type-families, type-level counterparts of
functions from the `Data.Char` module.
In contrast to Vieth’s approach, we use the same Char type and don’t
introduce the different `Character` kind. We provide slightly more helpers
to work with the Char kind, see below.
You may take a look at this merge request with proposed updates:
https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3598.

First of all, we overview the additional type families implemented by us in
this patch.

type family CmpChar (a :: Char) (b :: Char) :: Ordering

Comparison of type-level characters, as a type family. A type-level
analogue of the function `compare` specified for characters.

type family LeqChar (a :: Char) (b :: Char) :: Bool

This is a type-level comparison of characters as well. `LeqChar` yields a
Boolean value and corresponds to `(<=)`.

type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol

This extends a type-level symbol with a type-level character

type family UnconsSymbol (a :: Symbol) :: Maybe (Char, Symbol)

This type family yields type-level `Just` storing the first character of a
symbol and its tail if it is nonempty and `Nothing` otherwise.

Type-level counterparts of the functions `toUpper`, `toLower`, and
`toTitle` from 'Data.Char'.

type family ToUpper (a :: Char) :: Char

type family ToLower (a :: Char) :: Char

type family ToTitle (a :: Char) :: Char


These type families are type-level analogues of the functions `ord` and
`chr` from Data.Char respectively.

type family CharToNat (a :: Char) :: Nat

type family NatToChar (a :: Nat) :: Char


A type-level analogue of the function `generalCategory` from `Data.Kind`.

type family GeneralCharCategory (a :: Char) :: GeneralCategory


The second group of type families consists of built-in unary predicates.
All of them are based on their corresponding term-level analogues from
`Data.Char`. The precise list is the following one:

type family IsAlpha (a :: Char) :: Bool

type family IsAlphaNum (a :: Char) :: Bool

type family IsControl (a :: Char) :: Bool

type family IsPrint (a :: Char) :: Bool

type family IsUpper (a :: Char) :: Bool

type family IsLower (a :: Char) :: Bool

type family IsSpace (a :: Char) :: Bool

type family IsDigit (a :: Char) :: Bool

type family IsOctDigit (a :: Char) :: Bool

type family IsHexDigit (a :: Char) :: Bool

type family IsLetter (a :: Char) :: Bool


We also provide several type-level predicates implemented via the
`GeneralCharCategory` type family.

type IsMark a = IsMarkCategory (GeneralCharCategory a)

type IsNumber a = IsNumberCategory (GeneralCharCategory a)

type IsPunctuation a = IsPunctuationCategory (GeneralCharCategory a)

type IsSymbol a = IsSymbolCategory (GeneralCharCategory a)

type IsSeparator a = IsSeparatorCategory (GeneralCharCategory a)

Here is an example of an implementation:

type IsMark a = IsMarkCategory (GeneralCharCategory a)

type family IsMarkCategory (c :: GeneralCategory) :: Bool where

     IsMarkCategory 'NonSpacingMark       = 'True

     IsMarkCategory 'SpacingCombiningMark = 'True

      IsMarkCategory 'EnclosingMark        = 'True

     IsMarkCategory _                     = 'False

Built-in type families I described above are supported with the
corresponding definitions and functions in `compiler/GHC/Builtin/Names.hs`,
`compiler/GHC/Builtin/Types.hs`, and
`compiler/GHC/Builtin/Types/Literals.hs`.

In addition to type families, our patch contain the following updates:

   1.

    parsing the 'x' syntax
   2.

    type-checking 'x' :: Char
   3.

    type-checking Refl :: 'x' :~: 'x'
   4.

    Typeable / TypeRep support
   5.

    template-haskell support
   6.

    Haddock related updates
   7.

    tests


At the moment, the merge request has some minor imperfections for polishing
and improvement, but we have a prototype of a possible implementation.
The aim of my email is to receive your feedback on this patch.

Kind regards,
Danya Rogozin.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20200710/a169cb8a/attachment.html>