data Foo :: (forall a. a -> Maybe a) -> Type Neither Foo nor Foo 'Just is Typeable. There seems to be a certain sense to excluding Foo proper, because it can't be decomposed with Fun. But why not Foo 'Just? Is there a fundamental reason, or is that largely an implementation artifact? David Feuer Well-Typed, LLP _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
Trying to conclude Typeable Foo (or, if expanded with
-fprint-explicit-kinds, Typeable ((forall a. a -> Maybe a) -> Type) Foo) is beyond GHC's capabilities at the moment, as that would require impredicative polymorphism. This problem has arose in other contexts too—see Trac #13895 [1] for one example. I don't think you can conclude Typeable (Foo 'Just) either, since that requires concluding both Typeable Foo and Typeable 'Just, so you ultimately run into the same problem. While there an in-the-works plan to allow a limited form of impredicativity through explicit use of visible type application [2], my fear is that that wouldn't be enough to address the problem you've encountered, since there's no way to visibly apply @((forall a. a -> Maybe a) -> Type) to Typeable at the moment. To accomplish this, you would need visible kind application [3]. Ryan S. ----- [1] https://ghc.haskell.org/trac/ghc/ticket/13895 [2] https://ghc.haskell.org/trac/ghc/ticket/11319#comment:11 [3] https://ghc.haskell.org/trac/ghc/ticket/12045 _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
In reply to this post by David Feuer-2
I don't see why Typeable (Foo 'Just) requires that. I'd expect to get back a TrTyCon, not a TrApp. Some modifications to the structure of TrTyCon might be required. David Feuer Well-Typed, LLP -------- Original message -------- From: Ryan Scott <[hidden email]> Date: 9/24/17 10:08 AM (GMT-05:00) To: [hidden email] Subject: Re: Why isn't this Typeable? -fprint-explicit-kinds, Typeable ((forall a. a -> Maybe a) -> Type) Foo) is beyond GHC's capabilities at the moment, as that would require impredicative polymorphism. This problem has arose in other contexts too—see Trac #13895 [1] for one example. I don't think you can conclude Typeable (Foo 'Just) either, since that requires concluding both Typeable Foo and Typeable 'Just, so you ultimately run into the same problem. While there an in-the-works plan to allow a limited form of impredicativity through explicit use of visible type application [2], my fear is that that wouldn't be enough to address the problem you've encountered, since there's no way to visibly apply @((forall a. a -> Maybe a) -> Type) to Typeable at the moment. To accomplish this, you would need visible kind application [3]. Ryan S. ----- [1] https://ghc.haskell.org/trac/ghc/ticket/13895 [2] https://ghc.haskell.org/trac/ghc/ticket/11319#comment:11 [3] https://ghc.haskell.org/trac/ghc/ticket/12045 _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
In reply to this post by David Feuer-2
The problem is that to get Typeable (Foo 'Just), we need Typeable 'Just. However, the kind parameter for Typeable 'Just would be (forall a. a -> Maybe a), making the full constraint Typable (forall a. a -> Maybe a) 'Just. And saying that would be impredicative. In other contexts, 'Just *can* be Typeable, but it's 'Just invisibly instantiated at some monotype for `a`. So I think that this boils down to impredicativity and that the implementation is doing the right thing here. Richard
_______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
My example wasn't quite the one I intended (although I think it should
work as well, and it's simpler). Here's the sort of example I really intended: data Bar :: forall (j :: forall k. k -> Maybe k) (a :: Type). Proxy (j a) -> Type I would expect Bar :: Proxy ('Just Int) -> Type or, to abuse notation a bit, Bar @'Just @Int to be Typeable. What I'm really suggesting is that we should distinguish between things that are typeable and things that can be decomposed into typeable components. We already make a limited distinction here. For example, we have 'Just :: forall a. a -> Maybe a 'Just itself cannot be Typeable, but once it's applied to a kind variable, it is Typeable. 'Just @Int is Typeable even though that (kind) application cannot be broken with App. Similarly, I'd expect Foo 'Just to be Typeable even though that (type) application cannot be broken with App (or Fun). Putting things in terms of fingerprints, we can offer type-indexed fingerprints newtype Finger a = Finger Fingerprint for anything we can fingerprint. Is there any difficulty fingerprinting types like Foo 'Just and Bar @'Just @Int? Fingerprints are useful for lots of applications where decomposition isn't necessary. On Sunday, September 24, 2017 1:16:37 PM EDT Richard Eisenberg wrote: > The problem is that to get Typeable (Foo 'Just), we need Typeable 'Just. However, the kind parameter for Typeable 'Just would be (forall a. a -> Maybe a), making the full constraint Typable (forall a. a -> Maybe a) 'Just. And saying that would be impredicative. In other contexts, 'Just *can* be Typeable, but it's 'Just invisibly instantiated at some monotype for `a`. > > So I think that this boils down to impredicativity and that the implementation is doing the right thing here. > > Richard > > > On Sep 24, 2017, at 5:45 AM, David Feuer <[hidden email]> wrote: > > > > data Foo :: (forall a. a -> Maybe a) -> Type > > > > Neither Foo nor Foo 'Just is Typeable. There seems to be a certain sense to excluding Foo proper, because it can't be decomposed with Fun. But why not Foo 'Just? Is there a fundamental reason, or is that largely an implementation artifact? > > > > David Feuer > > Well-Typed, LLP > > _______________________________________________ > > ghc-devs mailing list > > [hidden email] > > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
I suppose this is conceivable, but it would complicate the representation and solver for TypeReps considerably. Do you have a real use case?
Richard > On Sep 25, 2017, at 2:28 PM, David Feuer <[hidden email]> wrote: > > My example wasn't quite the one I intended (although I think it should > work as well, and it's simpler). Here's the sort of example I really intended: > > data Bar :: forall (j :: forall k. k -> Maybe k) (a :: Type). Proxy (j a) -> Type > > I would expect > > Bar :: Proxy ('Just Int) -> Type > > or, to abuse notation a bit, > > Bar @'Just @Int > > to be Typeable. What I'm really suggesting is that we should distinguish between things that are typeable and > things that can be decomposed into typeable components. We already make a limited distinction > here. For example, we have > > 'Just :: forall a. a -> Maybe a > > 'Just itself cannot be Typeable, but once it's applied to a kind variable, it is Typeable. > 'Just @Int is Typeable even though that (kind) application cannot be broken with App. Similarly, I'd expect > Foo 'Just to be Typeable even though that (type) application cannot be broken with App (or Fun). > > Putting things in terms of fingerprints, we can offer type-indexed fingerprints > > newtype Finger a = Finger Fingerprint > > for anything we can fingerprint. Is there any difficulty fingerprinting types like Foo 'Just and > Bar @'Just @Int? Fingerprints are useful for lots of applications where decomposition isn't > necessary. > > On Sunday, September 24, 2017 1:16:37 PM EDT Richard Eisenberg wrote: >> The problem is that to get Typeable (Foo 'Just), we need Typeable 'Just. However, the kind parameter for Typeable 'Just would be (forall a. a -> Maybe a), making the full constraint Typable (forall a. a -> Maybe a) 'Just. And saying that would be impredicative. In other contexts, 'Just *can* be Typeable, but it's 'Just invisibly instantiated at some monotype for `a`. >> >> So I think that this boils down to impredicativity and that the implementation is doing the right thing here. >> >> Richard >> >>> On Sep 24, 2017, at 5:45 AM, David Feuer <[hidden email]> wrote: >>> >>> data Foo :: (forall a. a -> Maybe a) -> Type >>> >>> Neither Foo nor Foo 'Just is Typeable. There seems to be a certain sense to excluding Foo proper, because it can't be decomposed with Fun. But why not Foo 'Just? Is there a fundamental reason, or is that largely an implementation artifact? >>> >>> David Feuer >>> Well-Typed, LLP >>> _______________________________________________ >>> ghc-devs mailing list >>> [hidden email] >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> > > _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
In reply to this post by David Feuer-2
No. What led me down this path is that I was thinking about whether we could simplify the representation and reduce the TCB. The as-yet-incomplete ideas I had (largely based on the concept of using a constructor name as a singletons-style defunctionalization symbol) seem difficult to adapt to the generalization I describe, so I wanted to check first how much that matters. David Feuer Well-Typed, LLP -------- Original message -------- From: Richard Eisenberg <[hidden email]> Date: 9/25/17 2:42 PM (GMT-05:00) To: David Feuer <[hidden email]> Cc: Ben Gamari <[hidden email]>, [hidden email] Subject: Re: Why isn't this Typeable? Richard > On Sep 25, 2017, at 2:28 PM, David Feuer <[hidden email]> wrote: > > My example wasn't quite the one I intended (although I think it should > work as well, and it's simpler). Here's the sort of example I really intended: > > data Bar :: forall (j :: forall k. k -> Maybe k) (a :: Type). Proxy (j a) -> Type > > I would expect > > Bar :: Proxy ('Just Int) -> Type > > or, to abuse notation a bit, > > Bar @'Just @Int > > to be Typeable. What I'm really suggesting is that we should distinguish between things that are typeable and > things that can be decomposed into typeable components. We already make a limited distinction > here. For example, we have > > 'Just :: forall a. a -> Maybe a > > 'Just itself cannot be Typeable, but once it's applied to a kind variable, it is Typeable. > 'Just @Int is Typeable even though that (kind) application cannot be broken with App. Similarly, I'd expect > Foo 'Just to be Typeable even though that (type) application cannot be broken with App (or Fun). > > Putting things in terms of fingerprints, we can offer type-indexed fingerprints > > newtype Finger a = Finger Fingerprint > > for anything we can fingerprint. Is there any difficulty fingerprinting types like Foo 'Just and > Bar @'Just @Int? Fingerprints are useful for lots of applications where decomposition isn't > necessary. > > On Sunday, September 24, 2017 1:16:37 PM EDT Richard Eisenberg wrote: >> The problem is that to get Typeable (Foo 'Just), we need Typeable 'Just. However, the kind parameter for Typeable 'Just would be (forall a. a -> Maybe a), making the full constraint Typable (forall a. a -> Maybe a) 'Just. And saying that would be impredicative. In other contexts, 'Just *can* be Typeable, but it's 'Just invisibly instantiated at some monotype for `a`. >> >> So I think that this boils down to impredicativity and that the implementation is doing the right thing here. >> >> Richard >> >>> On Sep 24, 2017, at 5:45 AM, David Feuer <[hidden email]> wrote: >>> >>> data Foo :: (forall a. a -> Maybe a) -> Type >>> >>> Neither Foo nor Foo 'Just is Typeable. There seems to be a certain sense to excluding Foo proper, because it can't be decomposed with Fun. But why not Foo 'Just? Is there a fundamental reason, or is that largely an implementation artifact? >>> >>> David Feuer >>> Well-Typed, LLP >>> _______________________________________________ >>> ghc-devs mailing list >>> [hidden email] >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> > > _______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
In reply to this post by David Feuer-2
I think we're a long way off from supporting Typeable for higher-kinded types, so I wouldn't worry about that dark, spider-ridden corner. Richard
_______________________________________________ ghc-devs mailing list [hidden email] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs |
Free forum by Nabble | Edit this page |