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 FeuerWell-Typed, LLP
-------- Original message --------From: Richard Eisenberg
<r...@cs.brynmawr.edu> Date: 9/25/17 2:42 PM (GMT-05:00) To: David Feuer
<da...@well-typed.com> Cc: Ben Gamari <b...@smart-cactus.org>,
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 <da...@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 <da...@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@haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>
>
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
