#11342: Character kind -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: alexvieth Type: feature request | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: DataKinds Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #10776 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by thomie): * status: new => patch * keywords: => DataKinds * related: => #10776 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11342#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11342: Character kind -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: alexvieth Type: feature request | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: DataKinds Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #10776, #12162 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Before looking at implementation, let's think about design: Is there any reason the kind shouldn't be `Char`? `Symbol` is actually different from `String` (the former is monolithic while the latter is a list) and `Nat`, when it was invented, was different from any term-level type. But neither of these arguments apply to `Char`. I'm also trying to be forward thinking about naming. In my thoughts about DependentHaskell, I've envisioned using the `'` promotion operator (which already exists for data constructors) to promote term-level variables. In this way, instead of `ToUpper`, we would have `'toUpper`. Unlike with data constructors, the quote would be mandatory, because otherwise `toUpper` would look like a type variable. Of course, we don't have DependentHaskell and I wouldn't want this rather independent work to become dependent on DependentHaskell. But a small tweak now could make things line up nicely later. '''Proposal:''' * In a type, parse `'`''varid'' as a ''conid''. That means that a use of, say, `'foo` in a type would be in the same syntactic category as `Foo`. In particular, you would be able to say {{{ type family 'toUpper (c :: Char) :: Char }}} Before we have DependentHaskell, all of the `Data.Char` operations would indeed have to be re-implemented one level up. But if we name them according to this scheme, then when we do have DependentHaskell, we don't have to break all the code that uses promoted characters. My expectation would be that the type family declaration above would no longer work -- the type-level definition would be promoted from the term-level definition -- but clients don't need to change. Thoughts? As for the implementation, I'm sorry to be annoying, but could you post the patch to Phab? It's just so much easier to read there and comment on. Thanks. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11342#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11342: Character kind -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: alexvieth Type: feature request | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: DataKinds Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #10776, #12162 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by cactus): * cc: cactus (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11342#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11342: Character kind -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: alexvieth Type: feature request | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: DataKinds Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #10776, #12162 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by akio): * cc: akio (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11342#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11342: Character kind -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: alexvieth Type: feature request | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: DataKinds Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #10776, #12162 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by zyla): I think that using the promoted `Char` datatype is a good idea. I wouldn't however put in all the related type families (`ToUpper`, `IsAlpha` etc). I think it's better to provide type families for converting between `Char` and `Nat`, and let the user implement the needed functions at type level if desired. The motivation is having less code in the compiler. To sum up, my proposal is to have: 1. Promoted `Char` datatype (already there) 2. Character literal syntax in types 3. Type famililes for analyzing/constructing `Symbol`s: {{{ -- Pattern match a Symbol. 'Nothing when empty, 'Just '(head, tail) -- otherwise. type family UnconsSymbol (s :: Symbol) :: Maybe (Character, Symbol) -- Put a Character at the head of a Symbol. type family ConsSymbol (c :: Character) (s :: Symbol) :: Symbol }}} 4. Type families for converting between `Nat` and `Char`: {{{ type family CharToNat (c :: Char) :: Nat type familt NatToChar (n :: Nat) :: Char }}} @alexvieth: Are you planning to work on this? If not, would you mind if I took your patch, implemented the changes mentioned above and posted it to Phab? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11342#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11342: Character kind -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: alexvieth Type: feature request | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: DataKinds Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #10776, #12162 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by vagarenko): * cc: vagarenko (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11342#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler