Why isn't this Typeable?

[Richard Eisenberg]

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 <david at well-typed.com> 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 <rae at cs.brynmawr.edu>
> Date: 9/25/17 2:42 PM (GMT-05:00)
> To: David Feuer <david at well-typed.com>
> Cc: Ben Gamari <ben at smart-cactus.org>, ghc-devs at haskell.org
> 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 <david at well-typed.com> 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 <david at well-typed.com> 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
> >>> ghc-devs at haskell.org
> >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> >> 
> > 
> > 
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20170925/75e0da7a/attachment-0001.html>