[core libraries] Fwd: The Char Kind: proposal

[Emily Pillmore]

CC'ing @core-libraries-committee so we don't lose this. It's important work!

On Fri, Jul 10, 2020 at 12:02 PM, Daniel Rogozin < daniel.rogozin at serokell.io > wrote:

> 
> 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 (
> 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:
> 
> * 
> 
> parsing the 'x' syntax
> 
> 
> * 
> 
> type-checking 'x' :: Char
> 
> 
> * 
> 
> type-checking Refl :: 'x' :~: 'x'
> 
> 
> * 
> 
> Typeable / TypeRep support
> 
> 
> * 
> 
> template-haskell support
> 
> 
> * 
> 
> Haddock related updates
> 
> 
> * 
> 
> 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.
> 
> 
> 
> 
> 
> --
> You received this message because you are subscribed to the Google Groups
> "haskell-core-libraries" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to haskell-core-libraries+unsubscribe@ googlegroups. com (
> haskell-core-libraries+unsubscribe at googlegroups.com ).
> To view this discussion on the web visit https:/ / groups. google. com/ d/
> msgid/ haskell-core-libraries/ CAD_SdCWxBvh%2BU5k87CxZ3SOxqXC%2BmyvE9oh%3DzhMqV2HWe-vzag%40mail.
> gmail. com (
> https://groups.google.com/d/msgid/haskell-core-libraries/CAD_SdCWxBvh%2BU5k87CxZ3SOxqXC%2BmyvE9oh%3DzhMqV2HWe-vzag%40mail.gmail.com?utm_medium=email&utm_source=footer
> ).
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20200828/cb5384e3/attachment.html>