The Char Kind: proposal

[Carter Schonwald]

This is cool!

I do think that as ghc works today, these would have to definitely be wired
into ghc, and there’s of course the philosophical issue of unicode changing
over time.   But this would be a good thing to execute on and add to ghc.

We already have some baby stuff around strings/symbols at the type levle,
and work to support more human lanaguage type level computation sounds
legit!

On Thu, Aug 27, 2020 at 8:03 PM Emily Pillmore <emilypi at cohomolo.gy> wrote:

> 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.
>>
>> 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.
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>> --
>>
>>
>> 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 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/20200831/62dd6556/attachment.html>