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 > On Sep 25, 2017, at 3:00 PM, David Feuer <[email protected]> wrote: > > 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 <[email protected]> > Date: 9/25/17 2:42 PM (GMT-05:00) > To: David Feuer <[email protected]> > Cc: Ben Gamari <[email protected]>, [email protected] > Subject: Re: Why isn't this Typeable? > > 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 <[email protected]> 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 <[email protected]> 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 > >>> [email protected] > >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > >> > > > > >
_______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
