[GHC] #9568: Type classes that fully cover closed kinds
#9568: Type classes that fully cover closed kinds -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: feature request | Status: new Priority: lowest | Milestone: ⊥ Component: Compiler (Type | Version: 7.8.3 checker) | Operating System: Keywords: | Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: Difficulty: Unknown | None/Unknown Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- When we have a closed kind (I think data kinds may be the only ones that are closed?), and a type class that takes only that kind as a parameter, and we have instances of the typeclass for every type in the kind, it would be nice if we didn't have to list it in the context of every function that uses it. Example: in `GHC.TypeLits`, this relationship exists between `Nat` and `KnownNat`, `Symbol` and `KnownSymbol`. It also arises in many of my uses of data kinds, because I often end up with a `KnownX` class that provides term-level things related to whatever the type is. The constraints tend to end up everywhere, which is noisy. As far as I can tell they don't really carry any information: a `KnownNat n` constraint where `n :: Nat` should be able to be discharged in the same way that something like `Show Bool` is, because regardless of which `n` we pick we know there will be an instance. (This is trickier for closed kinds like `Nat` and `Symbol` than for user- defined ones through the data kinds feature, because the former are inhabited by infinitely many types.) Perhaps we could have a pragma to inform the compiler that this situation exists for a certain typeclass, which the compiler could check in finite cases (like the ones arising for user-defined data kinds) by enumerating all the cases. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9568 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9568: Type classes that fully cover closed kinds -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: feature | Status: new request | Milestone: ⊥ Priority: lowest | Version: 7.8.3 Component: Compiler | Keywords: (Type checker) | Architecture: Unknown/Multiple Resolution: | Difficulty: Unknown Operating System: | Blocked By: Unknown/Multiple | Related Tickets: Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by rwbarton): This is a natural thing to want but, alas, it's not so simple. It's not enough for the compiler to know that some instance exists. It has to know which instance to use, because the choice of instance affects the runtime semantics of the program. From a theory point of view, polymorphism over closed kinds has the same parametricity properties as polymorphism over open kinds like `*`. If I have a function `f :: forall (b :: Bool). Proxy b -> String` then `f`'s behavior cannot depend on the choice of `b`, so `f (Proxy :: Proxy False)` must be equal to `f (Proxy :: Proxy True)`, just like a function `g :: Maybe a -> String` must satisfy `g (Nothing :: Maybe Int)` = `g (Nothing :: Maybe Bool)`. From an implementation point of view there is no difference at all at runtime between `Proxy :: Proxy False` and `Proxy :: Proxy True`, so simply for that reason it's impossible for any function to distinguish them. But with a class constraint `C b`, even when `C` has instances for both `False` and `True`, `f`'s behavior can depend on `b`, as I'm sure you know. This is possible because the `C b` constraint gets translated to an extra value-level argument to the function. So, `f :: forall (b :: Bool). C b => Proxy b -> String` is really different from `f :: forall (b :: Bool). Proxy b -> String` even when `C b` is satisfied for each individual type `b :: Bool`. In light of all this, I'm not sure what change along the lines of your suggestion would be possible. IIRC Richard Eisenberg's "dependent Haskell" project includes a non-parametric universal quantifier; perhaps that is related. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9568#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9568: Type classes that fully cover closed kinds -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: feature | Status: new request | Milestone: ⊥ Priority: lowest | Version: 7.8.3 Component: Compiler | Keywords: (Type checker) | Architecture: Unknown/Multiple Resolution: | Difficulty: Unknown Operating System: | Blocked By: Unknown/Multiple | Related Tickets: Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): I agree fully with Reid (rwbarton). Those "class constraints" are really, under the hood, implicit parameters (dictionaries) passed around at runtime. Given that they have runtime significance, I don't think it's a good idea to hide them from the programmer. On the relationship to Pi-types: As described in [https://www.youtube.com/watch?v=O805YjOsQjI this video] and [wiki:DependentHaskell this wiki page], I'm working on a version of GHC that allows a type parameter to be made available at runtime. This feature could be used to simulate dictionary passing (I believe), by examining the type parameter at runtime and making decisions based on it. So, I guess this might improve the syntax a bit -- hard to say for sure at this point. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9568#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9568: Type classes that fully cover closed kinds -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: feature | Status: new request | Milestone: ⊥ Priority: lowest | Version: 7.8.3 Component: Compiler | Keywords: (Type checker) | Architecture: Unknown/Multiple Resolution: | Difficulty: Unknown Operating System: | Blocked By: Unknown/Multiple | Related Tickets: Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by dmcclean): Great point. Not sure what I was thinking, sorry. Regarding "If I have a function `f :: forall (b :: Bool). Proxy b -> String` then `f`'s behavior cannot depend on the choice of `b`", I think I got off track by thinking that the binding happens in two stages, and that when type type-level lambda was applied it could "pick" which term-level function it wanted to return after inspecting the type argument, and that all of that always happened at compile time. But it doesn't. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9568#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9568: Type classes that fully cover closed kinds
-------------------------------------+-------------------------------------
Reporter: dmcclean | Owner:
Type: feature | Status: new
request | Milestone: ⊥
Priority: lowest | Version: 7.8.3
Component: Compiler | Keywords:
(Type checker) | Architecture: Unknown/Multiple
Resolution: | Difficulty: Unknown
Operating System: | Blocked By:
Unknown/Multiple | Related Tickets:
Type of failure: |
None/Unknown |
Test Case: |
Blocking: |
Differential Revisions: |
-------------------------------------+-------------------------------------
Comment (by Herbert Valerio Riedel
#9568: Type classes that fully cover closed kinds
-------------------------------------+-------------------------------------
Reporter: dmcclean | Owner:
Type: feature | Status: new
request | Milestone: ⊥
Priority: lowest | Version: 7.8.3
Component: Compiler | Keywords:
(Type checker) | Architecture: Unknown/Multiple
Resolution: | Difficulty: Unknown
Operating System: | Blocked By:
Unknown/Multiple | Related Tickets:
Type of failure: |
None/Unknown |
Test Case: |
Blocking: |
Differential Revisions: |
-------------------------------------+-------------------------------------
Comment (by Herbert Valerio Riedel
#9568: Type classes that fully cover closed kinds -------------------------------------+------------------------------------- Reporter: dmcclean | Owner: Type: feature | Status: closed request | Milestone: ⊥ Priority: lowest | Version: 7.8.3 Component: Compiler | Keywords: (Type checker) | Architecture: Unknown/Multiple Resolution: wontfix | Difficulty: Unknown Operating System: | Blocked By: Unknown/Multiple | Related Tickets: Type of failure: | None/Unknown | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => wontfix Comment: I'm assuming that those two recent commits reference this ticket in error. And, it seems that the original poster agrees that the requested feature is invalid, so I'm closing this ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9568#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC