[GHC] #12162: Concatenation of type level symbols missing
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Type level string literals (of kind Symbol), should have a concatenation operation. It's very useful, e.g., in the library for strongly typed relations that we have. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by thomie): * status: new => closed * resolution: => duplicate Comment: I think #11342 already covers this request. Please reopen if I misunderstood. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by augustss): Having a Character kind would some cons/uncons would certainly make concatenation possible. But my request is more modest, easier to implement, more efficient, and easier to state injectivity properties of. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: duplicate | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by augustss): See comment. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by thomie): * status: closed => new * resolution: duplicate => -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: phadej Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): D2632 Wiki Page: | -------------------------------------+------------------------------------- Changes (by phadej): * owner: => phadej * differential: => D2632 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: phadej Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2632 Wiki Page: | -------------------------------------+------------------------------------- Changes (by phadej): * differential: D2632 => Phab:D2632 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: phadej Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2632 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Generally the patch looks good to me, thank you. But can we first agree about goals and nomenclature. * Minor: you use the term "concat" in the implementation, but the list `concat` function has type `[[a]] -> [a]` not `[a] -> [a] -> [a]`. We generally use "append" for the latter; e.g. `appendFS`. * In order to do this you have figured out how to add a new type-level operator to GHC. Is that written up on the wiki anywhere? If not it'd be great if you could do so? There are a number of separate things you have to do. [wiki:TypeNats] would be a good place to start, despite its Nat- sounding title. * More significant. You are introducing a type-level operator `(<>) :: Symbol -> Symbol -> Symbol`. Wouldn't `(++)` be more appropriate? It's type is very like `(++)`. The other use of `(<>)` that I know of is in the pretty printing library, where it has type `Doc -> Doc -> Doc` so there is precedent there. I think it partly depends on whether we are regarding `Symbol` as an opaque type; in which case we might want to keep `(++)` for appending type-level lists (or does it exist already?). But #11342 is (I think) arguing for a less opaque representation. * Incidentally I realise that I don't know how to find the Haddock docs for the functions available over `Symbol`.... I'm copying in the core libraries committee, since this is really their territory. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: phadej Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2632 Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: core-libraries-committee@… (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: phadej Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2632 Wiki Page: | -------------------------------------+------------------------------------- Comment (by phadej): * good point about `append` vs. `concat` , append will be definitely better * As said in the Phab, I mostly copied things from existing magic type families. E.g. there are comments like `(a + 5 ~ 8) => (a ~ 3)`, which I tried to reproduce for `(<>)`, but I didn't managed to find any tests exercising those code paths (I didn't spent too much time looking though). 1f77a5341cbd6649a6bc2af868002728cd79b9d7 patch added most of the `TcTypeNats.hs`, I guess it make sense to add refined parts of commit message to the wiki. Will do. * I personally think `(<>)` is more appropriate than `(++)`. I had an idea to make `(<>)` polykinded `:: forall k. k -> k -> k` with the `Symbol` instantiation as a magic one. But it seems to be easier to leave the abstracting part to the userland, and have magical monomorphic type. So it might make sense to not use any operator name at all, but a name like `AppendSymbol`, and define `<>` to work on symbols and lists in `base` or some other type-level trickery library. * FWIW, I think there aren't any other places with functions over `Symbol` than the ones in `GHC.TypeLits`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: phadej Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2632 Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I'm indifferent about what to name `(<>)`, but the fact that someone has objected to it means it might be worth starting a thread on the [https://mail.haskell.org/pipermail/libraries/ libraries mailing list] to figure out the community's opinion. I've heard convincing arguments for both `(<>)` and `(++)`. Or `(+++)`, which is what the [https://github.com/konn/ghc-typelits- symbols/blob/cd812f4cfc2e6816a18283a6a0e9bb2d9ea2905e/src/GHC/TypeLits/Symbols/Internal.hs#L6-L8 ghc-typelits-symbols] GHC plugin library has taken to calling this operation. Or `AppendSymbol`, if we really want to explore all options. If you wish to add tests for this feature, there is a portion of the GHC test suite located in `base` [http://git.haskell.org/ghc.git/tree/HEAD:/libraries/base/tests here]. And you're absolutely correct in observing that the `Symbol` API is quite feature-poor at the moment. OtToMH, there are only three useful operations over `Symbol`s in `base`: * You can check whether two symbols are equal (either through type-level equality or through [http://hackage.haskell.org/package/base-4.9.0.0/docs /GHC-TypeLits.html#v:sameSymbol sameSymbol]). * You can compare two symbols lexicographically with [http://hackage.haskell.org/package/base-4.9.0.0/docs/GHC- TypeLits.html#t:CmpSymbol CmpSymbol]. * You can convert a `KnownSymbol` to a `String` value with [http://hackage.haskell.org/package/base-4.9.0.0/docs/GHC- TypeLits.html#v:symbolVal symbolVal]. And that's about it. While it'd be nice to have promoted lists of `Char`s and just promote all operations over lists, that's much more work, and `Symbol`'s all we've got for now, so we might as well work with it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: phadej Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2632 Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Mailing list discussion about what to name it: https://mail.haskell.org/pipermail/libraries/2016-October/027386.html -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: phadej Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2632 Wiki Page: | -------------------------------------+------------------------------------- Comment (by ekmett): If we build in {{{#!hs type family (++) :: Symbol -> Symbol -> Symbol }}} that doesn't prevent it from later being used in a potential later or even third-party polykinded {{{#!hs type family (<>) :: k -> k -> k type instance (<>) = (++) }}} and it would be consistent with the fact that the other `GHC.TypeLits` such as `(+)` are all specific to one kind. That said, none of the existing machinery for `KnownNat` knows anything about `(+)`, so it'd be a leap to expect `KnownSymbol` to know about `(++)`. Also note that complicating evidence by giving it more internal hidden constructors like is used to deal with `Coercible` instances is actually bad for folks who use things like reflection to mimic this behavior or construct symbols at runtime today. As an aside, you can actually get type level symbol concatenation and tools for working with it out of the `constraints` package at least in HEAD today, but it doesn't have any compiler assistance. You have to explicitly use the various axioms and `appendSymbol` proofs rather explicitly to get the resulting `KnownSymbol` instances, but you can do it. https://github.com/ekmett/constraints/blob/master/src/Data/Constraint/Symbol... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: phadej Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2632 Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): Lennart, do you think you could give a bit more info about why you need this, for documentation purposes if nothing else? Also, I'm curious whether we could ''lose'' anything by revealing that `Symbol` is anything more than ordered. I don't know of anything, but that doesn't mean there isn't anything. Finally, are there other operations on symbols that would be useful? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: phadej Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2632 Wiki Page: | -------------------------------------+------------------------------------- Changes (by dfeuer): * component: Compiler => Compiler (Type checker) * milestone: => 8.2.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#12162: Concatenation of type level symbols missing
-------------------------------------+-------------------------------------
Reporter: augustss | Owner: phadej
Type: feature request | Status: new
Priority: normal | Milestone: 8.2.1
Component: Compiler (Type | Version: 8.0.1
checker) |
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D2632
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Ben Gamari
#12162: Concatenation of type level symbols missing -------------------------------------+------------------------------------- Reporter: augustss | Owner: phadej Type: feature request | Status: closed Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D2632 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: new => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12162#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC