{"action":"created","issue":{"url":"https://api.github.com/repos/goldfirere/singletons/issues/318","repository_url":"https://api.github.com/repos/goldfirere/singletons","labels_url":"https://api.github.com/repos/goldfirere/singletons/issues/318/labels{/name}","comments_url":"https://api.github.com/repos/goldfirere/singletons/issues/318/comments","events_url":"https://api.github.com/repos/goldfirere/singletons/issues/318/events","html_url":"https://github.com/goldfirere/singletons/issues/318","id":308129461,"number":318,"title":"Make Sing a type family","user":{"login":"RyanGlScott","id":2364661,"avatar_url":"https://avatars2.githubusercontent.com/u/2364661?v=4","gravatar_id":"","url":"https://api.github.com/users/RyanGlScott","html_url":"https://github.com/RyanGlScott","followers_url":"https://api.github.com/users/RyanGlScott/followers","following_url":"https://api.github.com/users/RyanGlScott/following{/other_user}","gists_url":"https://api.github.com/users/RyanGlScott/gists{/gist_id}","starred_url":"https://api.github.com/users/RyanGlScott/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/RyanGlScott/subscriptions","organizations_url":"https://api.github.com/users/RyanGlScott/orgs","repos_url":"https://api.github.com/users/RyanGlScott/repos","events_url":"https://api.github.com/users/RyanGlScott/events{/privacy}","received_events_url":"https://api.github.com/users/RyanGlScott/received_events","type":"User","site_admin":false},"labels":[{"id":20376948,"url":"https://api.github.com/repos/goldfirere/singletons/labels/enhancement","name":"enhancement","color":"84b6eb","default":true}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":7,"created_at":"2018-03-23T18:06:09Z","updated_at":"2018-04-06T18:02:28Z","closed_at":null,"author_association":"COLLABORATOR","body":"Currently `Sing` is a data family. But it might be more natural to make it a type family, for two reasons.\r\n\r\nOne reason is extremely practical. After a [recent GHC commit](http://git.haskell.org/ghc.git/commit/ffb2738f86c4e4c3f0eaacf0a95d7326fdd2e383), compiling the test files in the test suite on GHC HEAD is now agonizingly slow—to the point where Travis times out, in fact. It's all due to the fact that GHC's pattern-match coverage checker is currently ill equipped to deal with data families, and after that commit, we now _actually_ coverage-check generated definitions involving `Sing` data family instances, and that overwhelms the coverage checker. Thus, turning `Sing` into a type family would conveniently avoid that issue.\r\n\r\nAnother reason is that it might actually make the presentation of `Sing` much cleaner. In the early days of `singletons` (according to @goldfirere's recollection), `Sing` was chosen to be a data family because of the injectivity properties it had. But we could get the same injectivity properties if we just use:\r\n\r\n```haskell\r\ntype family Sing :: k -> Type\r\n```\r\n\r\nThen, instead of generating something like this for each `Sing` instance (using the data family presentation):\r\n\r\n```haskell\r\ndata instance Sing :: Bool -> Type where\r\n  SFalse :: Sing False\r\n  STrue :: Sing True\r\ntype SBool = (Sing :: Bool -> Type)\r\n```\r\n\r\nWe would generate this:\r\n\r\n```haskell\r\ndata SBool :: Bool -> Type where\r\n  SFalse :: SBool False\r\n  STrue :: SBool True\r\ntype instance Sing = SBool\r\n```\r\n\r\nMoreover, with a type family version of `Sing`, one can get away with this:\r\n\r\n```haskell\r\ntype instance Sing = (TypeRep :: TYPE rep -> Type)\r\n```\r\n\r\nWhich is pretty slick."},"comment":{"url":"https://api.github.com/repos/goldfirere/singletons/issues/comments/379330975","html_url":"https://github.com/goldfirere/singletons/issues/318#issuecomment-379330975","issue_url":"https://api.github.com/repos/goldfirere/singletons/issues/318","id":379330975,"user":{"login":"RyanGlScott","id":2364661,"avatar_url":"https://avatars2.githubusercontent.com/u/2364661?v=4","gravatar_id":"","url":"https://api.github.com/users/RyanGlScott","html_url":"https://github.com/RyanGlScott","followers_url":"https://api.github.com/users/RyanGlScott/followers","following_url":"https://api.github.com/users/RyanGlScott/following{/other_user}","gists_url":"https://api.github.com/users/RyanGlScott/gists{/gist_id}","starred_url":"https://api.github.com/users/RyanGlScott/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/RyanGlScott/subscriptions","organizations_url":"https://api.github.com/users/RyanGlScott/orgs","repos_url":"https://api.github.com/users/RyanGlScott/repos","events_url":"https://api.github.com/users/RyanGlScott/events{/privacy}","received_events_url":"https://api.github.com/users/RyanGlScott/received_events","type":"User","site_admin":false},"created_at":"2018-04-06T18:02:28Z","updated_at":"2018-04-06T18:02:28Z","author_association":"COLLABORATOR","body":"> What did you do about point (2)? I suppose we could generate those instances for each singleton separately. Would that be hard? Not sure.\r\n\r\nCurrently, nothing—I simply commented out the instances and dealt with it. I suppose we could just generate `TestEquality` and `TestCoercion` instances alongside each `SDecide` instance we generate, which wouldn't be too bad.\r\n\r\n> As for point (1), I see several options:\r\n> \r\n> A. Push to change GHC's treatment of ScopedTypeVariables. I think this may be challenging, as Simon likes this the way it is (I've tried, in the past, on this front -- but I didn't try very hard).\r\n> \r\n> B. Teach Template Haskell about named wildcards (which are essentially type variables that can stand for any type) and use them here. This has the noted downside of causing users to enable `-XPartialTypeSignatures -XNamedWildCards -Wno-partial-type-signatures` to use `singletons`. A variant on this is also to teach TH to enable flags and warning options, and then this option becomes considerably more attractive.\r\n> \r\n> C. Figure out what loophole allows GHC to accept https://github.com/goldfirere/singletons/issues/318#issuecomment-376613158 and exploit it.\r\n> \r\n> Probably, choice (C) is easiest, but also the least satisfying.\r\n\r\nI feel like I'd need to understand the typing rules behind pattern signatures (and why the loophole for https://github.com/goldfirere/singletons/issues/318#issuecomment-376613158 currently exists) before I could make a judgment on this. Something definitely smells wrong with the current state of affairs, but I'm not qualified enough to say where the stench is coming from.\r\n\r\n> I'm unconcerned about your point (3). Do whatever is easiest (probably exporting `Sing` from more places).\r\n\r\nThat would probably be best, yes.\r\n\r\n> However, before investing more energy into this: what concretely do we gain by this change? Yes, it's more theoretically satisfying and all, but are there other benefits? Perhaps allowing us to have `type instance Sing = (TypeRep :: Type -> Type)` is quite nice. And, of course, there's the performance issue, but that's really GHC's problem, not ours. (Well, not `singletons`'s at least.) Maybe getting the performance issue fixed is a high priority, forcing us down this road.\r\n\r\nIndeed, the performance issue is the primary motivation behind this. However, it's worth noting that the commit which caused the performance issue is [going to be reverted soon](https://phabricator.haskell.org/D4545), so that won't be quite as urgent after that happens.\r\n\r\nOther than that, the only benefits are really aesthetic in nature."}}
{"actor":{"display_login":"RyanGlScott"}}