[GHC] #10832: Generalize injective type families
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature | Status: new request | Priority: normal | Milestone: Component: Compiler | Version: 7.11 (Type checker) | Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Revisions: | -------------------------------------+------------------------------------- With injective type families we can now declare that type family result determines the arguments. But ITFs are not yet as expressive as functional dependencies. For example with FDs I can say: {{{#!hs data Nat = Zero | Succ a class Add a b r | a b -> r, r a -> b instance Add Zero b b instance (Add a b r) => Add (Succ a) b (Succ r) }}} Here we declare that the result and the first argument taken together uniquely determine the second argument. This is not currently possible with ITFs: {{{#!hs type family AddTF a b = r | r a -> b where AddTF Zero b = b AddTF (Succ a) b = Succ (AddTF a b) }}} But we want to be able to say that. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Revisions: -------------------------------------+------------------------------------- Changes (by jstolarek): * related: => #6018 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): -------------------------------------+------------------------------------- Comment (by jstolarek): For anyone interested, the development of this feature is happening here: https://github.com/jstolarek/ghc/tree/T10832-generalized-injectivity At the moment it just compiles but I hope this implementation becomes usable Real Soon Now. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): D1287 -------------------------------------+------------------------------------- Changes (by jstolarek): * differential: => D1287 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 -------------------------------------+------------------------------------- Changes (by jstolarek): * differential: D1287 => Phab:D1287 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Comment (by carter): I've hit needing this feature for what I was hoping would be pretty elementary code :( {{{ type family ReverseTC (a :: [ k ]) (res :: [ k ] ) = result where ReverseTC '[] res = res ReverseTC (a ': bs ) res = ReverseTC bs (a ': res) type family Reverse (a :: [k]) = (result :: [k]) where Reverse a = ReverseTC a '[] }}} I would like to explain to GHC that if i know a and result , or res and result, i know the remaining variable, so that my "stack safe" Reverse computation can also be treated as Injective (which it is! ) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Comment (by jstolarek): Carter, can you upload a self-contained piece of code? When we were working on injective type families we had a really hard time finding real- world examples where injectivity was necessary. Many people in the past claimed that they needed it but when we finally had the feature implemented few people could remember their use cases from the past. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Changes (by nfrisby): * cc: nfrisby (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): See comment:119 on #6018 for a use-case example. I think the latest version of all this is in the main repo, on branch `wip/T10832-generalised-injectivity` -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: TypeFamilies => TypeFamilies, InjectiveFamilies -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Possible use-case #13731 {{{#!hs type family ExtensionType ext a = res | res -> ext a data ListExtension type instance ExtensionType ListExtension a = [a] }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Comment (by lexi.lambda): I might have a use case for this, but I’m not smart enough to understand if my problem would be solved by this feature or not. Basically, I have a type family for type-level append: {{{ #!hs type family xs :++: ys where '[] :++: ys = ys (x ': xs) :++: ys = x ': (xs :++: ys) }}} This family is not injective, but if you know the result and one of the two inputs, you can deduce the other one. Therefore, I would like to be able to write the dependency annotation `r xs -> ys, r ys -> xs`. I have written a function that uses `:++:` in its type signature, which currently looks like this: {{{ #!hs forall g r a f. (forall v. f v -> Eff (g :++: r) v) -> Eff (f ': r) a -> Eff (g :++: r) a }}} Currently, this signature is ambiguous. However, notably, we know `r`, and in the location this function is used, we also know `g :++: r`. Therefore, my hope is that with this feature, I could use this function, and `g` could be inferred. Currently, however, I have to use `TypeApplications` to pick `g` explicitly, even though the type seems “obvious” to the programmer at its use site (since it very explicitly duplicates type information in an adjacent top-level annotation). I don’t know enough to know if such an annotation would actually allow such a thing or not, or if this is even applicable in my use case, but I thought I would offer the example anyway, since it sounds like this feature is in need of motivating examples. (I can also try and come up with a smaller, self-contained example if I’m not totally off base and that would, in fact, be relevant/helpful.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): comment:13 looks like a use-case for injectivity to me. comment:9 has a fairly well-advanced implementation, just needs completing. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Changes (by lexi.lambda): * cc: lexi.lambda (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): comment:13 is asking for injectivity from result with ''either'' argument to the other. Notice the O.P. for `AddTF` only considers result & first argument `->` second arg. I see a problem. In instances {{{ type family xs :++: ys = r | r xs -> ys, r ys -> xs where -- both injectivities '[] :++: ys = ys (x ': xs) :++: ys = x ': (xs :++: ys) }}} Under the injection `r ys -> xs`, I think GHC will not be able to see the 'apartness' in the two equations. That is, it won't be able to disprove `ys ~ (x ': (xs :++: ys))`. Yes we know they can't unify, but GHC sees `:++:` as a Type Function, not a (proto-)constructor. Speculative remedy [https://github.com/AntC2/ghc-proposals/blob/instance- apartness-guards/proposals/0000-instance-apartness-guards.rst#injective- type-families proposed here], for the `AddTF` example. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Are we exploring avenues like [https://ghc.haskell.org/trac/ghc/ticket/6018#comment:48 head-injectivity] or partial injectivity? Richard's example tells us `x ~ Just y` if `F x ~ True` {{{#!hs type family F a where F (Just x) = True F Nothing = False }}} but similarly {{{#!hs type family G a where G (Just x) = (x, x) G Nothing = (Int, Int) }}} means `x ~ Int` if `G (Just x) ~ (Int, Int)` — is that useful? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: jstolarek Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): I haven't found so many uses for this, but I wanted to try this lately {{{#!hs -- Free :: (Type -> Constraint) -> (Type -> Type) -- Forget :: (Type -> Constraint) -> (Type -> Type) newtype Free cls a = Free (forall xx. cls xx => (a -> xx) -> xx) type family Forget cls free = res | res cls -> free where Forget cls (Free cls a) = a }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10832: Generalize injective type families -------------------------------------+------------------------------------- Reporter: jstolarek | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Keywords: TypeFamilies, Resolution: | InjectiveFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #6018 | Differential Rev(s): Phab:D1287 Wiki Page: | -------------------------------------+------------------------------------- Changes (by jstolarek): * owner: jstolarek => (none) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10832#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC