Why isn't this Typeable?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
8 messages Options
Reply | Threaded
Open this post in threaded view
|

Why isn't this Typeable?

David Feuer-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Why isn't this Typeable?

Ryan Scott
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
Reply | Threaded
Open this post in threaded view
|

Re: Why isn't this Typeable?

David Feuer-2
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)
Subject: Re: Why isn't this Typeable?

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

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Why isn't this Typeable?

Richard Eisenberg-4
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

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
Reply | Threaded
Open this post in threaded view
|

Re: Why isn't this Typeable?

David Feuer-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Why isn't this Typeable?

Richard Eisenberg-4
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
Reply | Threaded
Open this post in threaded view
|

Re: Why isn't this Typeable?

David Feuer-2
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?

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
Reply | Threaded
Open this post in threaded view
|

Re: Why isn't this Typeable?

Richard Eisenberg-4
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

On Sep 25, 2017, at 3:00 PM, David Feuer <[hidden email]> 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 <[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?

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