Re: Why isn't this Typeable?

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 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 Date: 9/25/17 2:42 PM (GMT-05:00) To: David Feuer Cc: Ben Gamari , ghc-devs@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 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 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs