[GHC] #15183: Expose the SNat type and the natSing method
#15183: Expose the SNat type and the natSing method -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: feature | Status: new request | Priority: normal | Milestone: 8.6.1 Component: Core | Version: 8.2.2 Libraries | 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: -------------------------------------+------------------------------------- Currently, neither the `SNat` type nor the `natSing` method of `KnownNat` are exported from `GHC.TypeLits`. This is weird and awkward. There's no apparent reason not to expose the `SNat` ''type'', although it may make sense not to expose its definition. It also could possibly make sense not to expose the fact that `natSing` is a ''method'' of `KnownNat`, but there's no apparent reason not to export a function with its type. Can we just do those? 1. Export the `SNat` type. 2. Export a function with the type of `natSing`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15183 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15183: Expose the SNat type and the natSing method -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.6.1 Component: Core Libraries | Version: 8.2.2 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: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): I don't necessarily object to this idea, but what exactly can one do with an `SNat` if it's exported abstractly? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15183#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15183: Expose the SNat type and the natSing method -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.6.1 Component: Core Libraries | Version: 8.2.2 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: | -------------------------------------+------------------------------------- Comment (by dfeuer): Well, clearly I missed a step. We'd also want a function to convert an `SNat` to a `Natural`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15183#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15183: Expose the SNat type and the natSing method -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.6.1 Component: Core Libraries | Version: 8.2.2 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: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): OK. Is your intention to provide an alternative to the current `Proxy`-based API? (For instance, `natVal :: KnownNat n = Proxy n -> Natural`, and you're suggesting to augment it with something like `fromNatSing :: SNat n -> Natural`?) If so, it may also be worth considering adding `SNat`-consuming counterparts to `sameNat` and `someNatVal` (the latter of which would require something like `data SomeNatSing`, which is like `SomeNat`, but having an `SNat` as a field instead of `Proxy`). Also, `KnownSymbol`/`symbolSing` has similar design considerations. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15183#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15183: Expose the SNat type and the natSing method -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.6.1 Component: Core Libraries | Version: 8.2.2 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: | -------------------------------------+------------------------------------- Comment (by goldfire): This was a design decision. In 2012 or so, Iavor was developing the TypeLits interface simultaneously with my development of singletons. We wanted to have one `Sing`, shared between the TypeLits stuff (built into GHC) and the singletons stuff (external). But the design considerations pulled at each other -- especially because `singletons` could make changes much more quickly than GHC could. So, instead of having built-in singletons and external singletons, it was decided to hide the built-in ones. Maybe now that we have more experience, this decision could be updated... but I still think that introducing any singletons into `base` will start a chain reaction of other feature requests. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15183#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15183: Expose the SNat type and the natSing method -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.6.1 Component: Core Libraries | Version: 8.2.2 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: | -------------------------------------+------------------------------------- Comment (by dfeuer): goldfire, there are already two singletons for these, but one is uncomfortably buried where we need `unsafeCoerce` to get at it. Since we have built-in support for `Nat`, `Symbol`, `KnownNat`, and `KnownSymbol`, I don't really see the slippery slope. `singletons` should be able to use a newtype instance around the one in `base`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15183#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC