Opened 4 years ago
Closed 3 years ago
#10343 closed feature request (wontfix)
Make Typeable track kind information better
Reported by: | oerjan | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.2.1 |
Component: | Compiler | Version: | 7.10.1 |
Keywords: | Typeable | Cc: | Ptharien's, Flame, oerjan, shachaf, int-e, dterei, RyanGlScott, sweirich |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | typeOf :: Typeable (a::k) => Proxy a -> TypeRep |
Blocked By: | Blocking: | ||
Related Tickets: | #9858, #11011 | Differential Rev(s): | |
Wiki Page: |
Description (last modified by )
(EDIT: My long rambling seems to have been confusing, so a summary:
I think that the type inference and runtime representation should support constructing Typeable (T :: k)
, even when k
contains kind variables that are only mentioned in other Typeable
constraints not necessarily involving the type constructor T
. This will allow simple composition with polymorphic type constructors like Proxy
and Typeable
to work more naturally, but also more complicated things.)
With all the apparent exploitable bugs now fixed, #9858 seems to be settling down. Simon P.J. asked me to make a new ticket for some quibbles I still have with limitations of the new design. These started with some examples that I discussed there pre-implementation with Richard Eisenberg, and which he concluded could be supported by a "sufficently smart solver".
In the new (current) design, a TypeRep
does contain kind information, which as I understand it is a list of KindRep
s for the explicit kind parameters applied to the type constructor after type inference. This is sufficient to prevent confusing the same type constructor used at different kinds, and also easily supports type application provided the TypeRep
s of the parts are known. For this, the internal Typeable
constraint solver only ever needs to combine TypeRep
s, never decompose them.
Since no one else complained in #9858, I assume this is enough for what people are currently using Typeable
for. However:
I think the current TypeRep
representation for Typeable (a :: k)
doesn't contain enough information to generally extract the KindRep
for k
itself, much less to decompose it, even if the internal Typeable
solver were to try. This prevents some polykinded code that is intuitively sound, and which "worked" in the old system, although if only because it didn't try to track kinds at all.
For example, the following expression, with PolyKinds
enabled:
typeOf :: Typeable a => Proxy a -> TypeRep
In the old system, this worked simply by combining the TypeRep
for Proxy
with the TypeRep
for a
. But in the new system, it fails, because the TypeRep
for Proxy
needs to know the kind of a
, which is neither statically known nor available from the TypeRep
of a
. You would need to have compile-time information about the type constructor of a
to even know how to build the KindRep
from the kind arguments.
This problem with constructing TypeRep
s would arise whenever a polykinded type constructor is applied to a type whose kind is not a known monomorphic one. The second similar one I can think of is
typeRep :: Typeable a => Proxy (Typeable a) -> TypeRep
In an ideal system, we can also find use cases that require not just extracting the KindRep
for a type, but also decomposing it. Here is my very hypothetical kitchen sink example from 46:ticket:9858 (this example was made up as a test case before I knew what the new solver would support):
{-# LANGUAGE PolyKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE AutoDeriveTypeable #-} import Data.Typeable newtype C a b = C () step :: Proxy (a :: [k] -> *) -> Proxy (C a :: [k -> *] -> *) step Proxy = Proxy nest :: Typeable (a :: [k] -> *) => Int -> Proxy a -> TypeRep nest 0 x = typeRep x nest n x = nest (n-1) (step x) main = print $ nest 10 (Proxy :: Proxy (C () :: [()] -> *))
Here, to make this compile, the solver would need to derive Typeable (C a :: [k -> *] -> *]
from Typeable (a :: [k] -> *)
, which at runtime requires first extracting the KindRep
of k
from the TypeRep
of a
, and then building the TypeRep
for the correctly kinded C
. At least the former part seems essentially impossible with the current TypeRep
representation, even with a more clever solver.
Change History (40)
comment:1 Changed 4 years ago by
Related Tickets: | 9858 → #9858 |
---|
comment:2 Changed 4 years ago by
Cc: | shachaf added |
---|
comment:3 Changed 4 years ago by
comment:4 Changed 4 years ago by
Here's a strange thought: once we have * :: *
, does Typeable k a
imply Typeable * k
? It probably should. But then we would have
class Typeable k => Typeable (a :: k) where ...
which has a superclass cycle. The cycle is benign because we know that all kinds have type *
, but it still is a curious beast.
Of course, this isn't necessary, but it would be nice.
comment:5 follow-up: 6 Changed 4 years ago by
I'm assuming that much of what Oerjan wants will "just work" once we have Richard's kind equalities. Right Richard?
But not, perhaps, kindRep
which I do not fully understand. I wonder if we might address kindRep
as part of the overhaul sketched in this wiki page about Typeable? The plan there is to move to type-indexed type representations.
- What would
kindRep
look in that context? - How would you use
kindRep
?
A new subsection on that page might be useful.
Simon
comment:6 Changed 4 years ago by
Replying to simonpj:
I'm assuming that much of what Oerjan wants will "just work" once we have Richard's kind equalities. Right Richard?
But not, perhaps,
kindRep
which I do not fully understand.
I'm not sure exactly what "much of what Oerjan wants" refers to, so I can't make a claim one way or the other. I can say that the feature requested in this ticket will not just work in my branch.
The problem is that if we have a TypeRep
for some time a
of kind k
, there is no way, at runtime, to extract a TypeRep
for k
. TypeRep
s simply don't store enough information to do this. Fixing this should be straightforward, and I believe is totally orthogonal to anything dealing with my branch. (Well, not totally orthogonal, because in my branch kindRep (kindRep <<anything>>)
is a TypeRep
for *
, and today it would be a TypeRep
for BOX
. But this matters little.) Coming up with an API design is a touch harder, but I don't think it should be too bad, and it remains independent from the TTypeRep a
story.
Oerjan, you're a (the?) client of all this. Propose an API design. :)
comment:7 Changed 4 years ago by
I am not sure I can be called a client, I don't have actual useful code hinging on this. As a hobbyist, I spend more time thinking about Haskell than actually programming in it.
I think that simply adding kindRep :: TypeRep -> TypeRep
as a field of TypeRep
would make the necessary information available at runtime. This ought to fit just as well into the current design as into the proposed TTypeRep
on the wiki. I also have a hunch this might make the already existing list of KindRep
s redundant.
The question of how to make the Typeable
solver make use of that information for building kind evidence seems to me like the more complicated part of this.
Just to prove it is possible in principle, I'll restate my mock representation from back in 48:ticket:9858:
class (KindableParts a, a ~ Proxy) => Kindable (a :: k -> *) where type KindableParts a :: Constraint kindRep :: KindRep a class Kindable (Proxy :: k -> *) => Typeable (a :: k) where typeRep :: proxy a -> TypeRep
This worked well enough to be a basis for running my kitchen sink test case in 7.8.3. However, it doesn't support Richard's ideas for avoiding exposing "Kindable
" constraints when doing type inference. And of course the representation's made for reusing already existing type features rather than for efficiency.
comment:8 Changed 4 years ago by
I was using "what Oerjan wants" as shorthand for the Description of this ticket. For exmaple, he wants the expression
typeRep :: Typeable a => Proxy a -> TypeRep
to typecheck. And it think it will when Richard is done. Similarly perhaps other items on his wish list above. Perhaps it would help to edit the description to enumerate "Wish 1", "Wish 2" etc?
In "Wish n" he is asking for kindRep
, for reasons I do not understand. Maybe you can give a use-case? And better still, what would it look like in the context of type-indexed type representations described in wiki:Typeable?
Simon
comment:9 Changed 4 years ago by
I knew I shouldn't have rambled on so much in my post... the mention of extracting KindRep
was not a direct wish, more my explanation of why the current design doesn't handle my test cases. As in, it would be needed to implement a solution to them.
So I guess a shorter summary of what I want is in order:
I want that the type inference and runtime representation should support constructing Typeable (T :: k)
, even when k
contains kind variables that are only mentioned in other Typeable
constraints not necessarily involving the type constructor T
.
(This assumes that type application keeps working as well as it does. Type constructors are the base case which now sometimes doesn't work.)
This is, as far as I can see, precisely what is needed to get things like typeOf :: Typeable a => Proxy a -> TypeRep
or typeRep :: Typeable a => Proxy (Typeable a) -> TypeRep
to work, but it would also enable much more contrived things like my kitchen sink example.
comment:10 Changed 4 years ago by
Description: | modified (diff) |
---|
comment:11 Changed 4 years ago by
Description: | modified (diff) |
---|
comment:12 follow-up: 15 Changed 4 years ago by
Milestone: | → 7.12.1 |
---|---|
Owner: | set to goldfire |
This all continues to seem straightforward to me, but I maintain (in contrast to Simon's claim in comment:8) that this is separate from kind equalities.
My implementation approach would be, as oerjan suggests, adding a kindRep
field in TypeRep
. This can be done today.
Then, define
class Typeable k => Typeable (a :: k) where ... -- probably not possible until I merge
This appears to be a superclass cycle, but we know it doesn't induce infinite regress because the kind of a kind is always *
. So, we arrange to have this definition accepted.
Then, the solver will just do the right thing. When we have a given Typeable (a :: k)
constraint, the solver will spit off a Typeable (k :: *)
constraint. We may have to arrange for the solver not to then spit off a (harmless, but potentially confusing) Typeable (* :: *)
constraint.
To work with typeOf :: Typeable a => Proxy a -> TypeRep
... well it will all just work. Typechecking this expression leads to
[G] Typeable (a :: k) [W] Typeable (Proxy (a :: k))
After a little work, the solver arrives at
[G] Typeable (a :: k) [G] Typeable (k :: *) [W] Typeable (Proxy :: k -> *) -- the Typeable solver doesn't decompose kind applications [W] Typeable (a :: k)
The wanteds are easily solved from the givens.
Since I'm the one with the plan, sounds like I should be the one to execute the plan. But probably only after I merge, since this isn't something we need today.
comment:13 follow-up: 16 Changed 4 years ago by
Can I make two pleas?
- Could we cast this discussion in the language of type-indexed type representations
TTypeRep
, in Typeable? ATTypeRep a
is very likeTypeable a
, but has the very great merit of being an ordinary data value.Typeable a
is just the implicit version of it. You can get from one to the other viatTypeRep
:class Typeable a where tTypeRep :: TTypeRep a
By using an ordinary data value we get away from talking about classes or superclasses or solvers or whatnot. Once we know, with forensic precision, whatTTypeable a
should do, then we can think about how the solver might generateTypeable a
dictionaries, which are simply containers for aTTypeable a
value.
- Can we keep
TTypeRep
abstract, so instead of talking about what it "contains" we speak entirely in terms of what functions are available over it?decomposeFun
is one such function. Now, forkindRep
I think you are asking for a functionkindRep :: forall (a::k). TTypeRep a -> TTypeRep k
And indeed it seems plausible that we should provide such a function, although I have seen no examples whatsoever of why it might be useful. (Producing aTypeRep
only to print it does not count; there are easier ways of producing that sequence of characters.)
I'm afraid I found the summary entirely opaque "The type inference and runtime representation should support constructing Typeable (T :: k)
, even when k contains kind variables that are only mentioned in other
Typeable
constraints not necessarily involving the type constructor T
. This will allow simple composition with polymorphic type constructors like Proxy
and Typeable
to work more naturally, but also more complicated things." What do you mean by "simple composition"? What do you mean by "more complicated things"?
Don't answer directly: rather, just give a sequence of examples that you think should work. That will show me what "simple composition" means, rather than telling me!
comment:14 Changed 4 years ago by
Cc: | int-e added |
---|
comment:15 Changed 4 years ago by
Replying to goldfire:
This all continues to seem straightforward to me, but I maintain (in contrast to Simon's claim in comment:8) that this is separate from kind equalities.
Whew, I was starting to worry.
[G] Typeable (a :: k) [G] Typeable (k :: *) [W] Typeable (Proxy :: k -> *) -- the Typeable solver doesn't decompose kind applications [W] Typeable (a :: k)The wanteds are easily solved from the givens.
Looks good, although note that as we discussed in #9858, the kitchen sink example would require actually decomposing Typeable
kinds.
In principle so does normal type application, once you include kindRep
:
(Typeable (a :: k1 -> k2), Typeable (b :: k1)) => Typeable (a b :: k2)
The only plausible source for the kindRep
of a b
is to decompose the kind information in Typeable a
. Although I guess type application can still be a special case.
Since I'm the one with the plan, sounds like I should be the one to execute the plan. But probably only after I merge, since this isn't something we need today.
:)
comment:16 Changed 4 years ago by
Replying to simonpj:
I made a long reply, forgot to copy to clipboard before submitting, and had trac give me an error message involving TLS, forgetting everything.
comment:17 follow-up: 18 Changed 4 years ago by
I've updated Typeable. See the new Proposed API section, and the new Step 3.
comment:18 Changed 4 years ago by
Replying to goldfire:
I've updated Typeable. See the new Proposed API section, and the new Step 3.
I'd like to note that if the proposed API is to help with Step 3 aka this ticket, either trCon
or your suggested tyConRep
needs to take a TTypeRep k
argument.
The "How can we get a TTyCon for a known-at-compile-time tycon?" was something I also stumbled on when trying to think of an API. Curiously if you simplify this a bit by removing TTyCon
(>_> <_<
), there is a nice end-user way of writing this from what's on the wiki page:
x :: TTypeRep k -> TTypeRep (Proxy :: k -> *) x tt = withTypeable tt tTypeRep
Of course this just calls back into the entire machinery that's being implemented, so cannot be used as a basis. However, it means that the primitive desugaring of this may not need to be exposed to users.
comment:19 Changed 4 years ago by
Cc: | dterei added |
---|
comment:20 Changed 4 years ago by
Cc: | Ptharien's Flame added |
---|
comment:21 Changed 4 years ago by
Cc: | RyanGlScott added |
---|
comment:23 Changed 4 years ago by
Cc: | sweirich added |
---|
comment:24 Changed 4 years ago by
I've been playing around with various ways that we could achieve this. As far as I can tell there are two options,
- Encode type constructor kinds into
TyCon
and reconstruct applications from these at runtime. This would require thatTyCon
get a bit larger, and would need to include aTypeRep
, which is unfortunate as this cost is paid by all users, regardless of whether they useTypeable
.
- Construct the kind representation at when we are asked to construct a
Typeable
dictionary.
At the moment I'm leaning towards the second approach (and have a broken implementation in Phab:D1837).
The trouble is that you need to be very careful when handling recursive kinding relationships. Consider, for instance, these examples:
(->) :: (->) * (* -> *) TYPE :: Levity -> TYPE 'Lifted
Here the types we are trying to derive kind representations for appear in their own kinds. This causes trouble in solving for these representations:
Currently we construct Typeable
evidence by decomposing type applications until we hit a tycon. One way to account for kind representations would be to require that when generating evidence for Typeable (t :: k)
we also generate evidence for Typeable k
. However, if we do this naively we end up sending the solver in a loop. Consider the case we are asked to solve for Typeable (Int -> Bool)
. Evidence construction would roughly proceed as follows,
want (Typeable (Int -> Bool :: *)) want (Typeable ((->) :: (* -> * -> *)) -- Normally this isn't a problem: -- since (->) is a TyCon, we could -- just stop here; but... -- now we need a kind representation want (Typeable (* -> * -> *)) want (Typeable ((->) * (* -> *))) -- again we decompose want (Typeable (->)) want (Typeable (* -> * -> *)) -- again solve for kind of (->) ... -- now we are in a loop...
Likewise, we can also get non-trivial cycles,
Levity :: TYPE 'Lifted TYPE :: Levity -> TYPE 'Lifted 'Lifted :: Levity
One way to address this issue would be to manually define these representations (just as we did before my recent solution to #11120), allowing us to tie the knot. This is a bit frustrating, however, as then we end up yet again having to manually define a handful of representations (and now their kind representations as well).
It would be nice if we could convince the solver to consider things like Typeable (->)
as solved when it encounters them; then next time it encounters this constraint it can simply use the evidence it generated earlier. Desugaring would then involve generating a recursive binding set containing all of the needed Typeable
dictionaries.
It's also possible that I have fundamentally misunderstood something here. If so, please feel free to say so.
comment:25 Changed 4 years ago by
I'm lost on this thread. Can someone re-state what the specification is? And do so without reference to the preceding 24 comments. Just a free-standing description of the problem we are trying to solve. I can't begin to think about an implementation until I'm clear about specification.
Also, can you do that in the light of the (recently-published) A reflection on types? It describes the story about type representation that I hope to get into HEAD once 8.0 is out of the way.
Thanks!
comment:26 Changed 4 years ago by
My goal was to augment the existing Typeable
interface with a means of extracting the kind of the type represented by a given TypeRep
. That is,
-- The current (non-type-indexed) TypeRep machinery data TypeRep type KindRep = TypeRep typeRep :: Typeable a => Proxy a -> TypeRep -- I wanted this... typeRepKind :: TypeRep -> KindRep
As far as I can tell, the semantics of typeRepKind
should be clear so long as we are only talking about monomorphically kinded types. For instance,
kindRep :: Typeable a => Proxy a -> KindRep kindRep = typeRepKind . typeRep kindRep (Proxy :: Proxy Int) == * kindRep (Proxy :: Proxy Int#) == TYPE 'Unlifted kindRep (Proxy :: Proxy '[4]) == '[Nat] kindRep (Proxy :: Proxy (4 ':)) == '[Nat] -> '[Nat] kindRep (Proxy :: Proxy []) == * -> * kindRep (Proxy :: Proxy [Int]) == * kindRep (Proxy :: Proxy ((->) Int)) == * -> * kindRep (Proxy :: Proxy Eq) == * -> Constraint kindRep (Proxy :: Proxy (':)) insoluble kindRep (Proxy :: Proxy 'Just) insoluble
Sorry if the above is a bit hand-wavy. I was merely looking for a nice weekend project; my experience in the typechecker is quite limited (although I'd love for that to change).
I have not thought much about this might fit in to the new type-indexed TypeRep
.
comment:27 Changed 4 years ago by
Perhaps something like this?
data Fingerprint = Fingerprint {- Int -} data TyCon a = TyCon Fingerprint String data TypeRep (a :: k) where TypeCon :: TyCon a -> TypeRep k -> TypeRep (a :: k) TypeApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1). TypeRep (a :: k1 -> k2) -> TypeRep (b :: k1) -> TypeRep (a b) class Typeable k => Typeable (a :: k) where typeRep :: TypeRep a typeRepKind :: forall (k :: *). forall (a :: k). TypeRep a -> TypeRep k typeRepKind (TypeCon _ k) = k typeRepName :: TypeRep a -> String typeRepName (TypeCon (TyCon _ n) _) = n
Unfortunately this currently doesn't compile due to the overly restrictive kind that we give to (->)
, * -> * -> *
. I would have thought this would be more polymorphic. There is a small note about this in TysPrim
,
You might think that
(->)
should have type?? -> ? -> *
, and you'd be right. But if we do that we get kind errors when sayinginstance Control.Arrow (->)because the expected kind is
* -> * -> *
. The trouble is that the expected/actual stuff in the unifier does not go contra-variant, whereas the kind sub-typing does. Sigh. It really only matters if you use(->)
in a prefix way, thus:(->) Int# Int#
. And this is unusual. because they are never in scope in the source
The reference to kind sub-typing makes me suspect that this restriction is no longer true. I've not yet tried lifting it, however.
comment:28 Changed 4 years ago by
OK, so the payload is that you want
typeRepKind : forall (k::*). forall (a::k). TypeRep a -> TypeRep k
At least I think that's the right type.
That's a nice short specification. I hope that it would not be too hard to implement.
The whole project of moving from the existing to the new TypeRep
needs someone to lead it; maybe that can be your weekend project! The key ticket is #11011, and wiki page Typeable.
comment:29 Changed 4 years ago by
The whole project of moving from the existing to the new TypeRep needs someone to lead it; maybe that can be your weekend project!
Indeed I have been eyeing it. I thought exposing kind representations would be a good warm-up, although at various points over the weekend I've considered going all-in and moving ahead with the new TypeRep
.
comment:30 Changed 4 years ago by
Let's not implement typeRepKind
in the existing TypeRep
setup. First move to the new one!
comment:31 Changed 4 years ago by
Keywords: | Typeable added |
---|
comment:32 Changed 4 years ago by
Milestone: | 8.0.1 → 8.2.1 |
---|
This bug won't be fixed in 8.0.1; bumping to 8.2.
comment:33 Changed 3 years ago by
Related Tickets: | #9858 → #9858, #11011 |
---|
For the record, this will be addressed in the solution of #11011 which should be coming in GHC 8.2. See Typeable/BenGamari for details.
comment:34 Changed 3 years ago by
Resolution: | → duplicate |
---|---|
Status: | new → closed |
Given that the type-indexed Typeable rework will provide support for pulling the kind out of a TypeRep
I'm going to close this as a duplicate.
comment:35 Changed 3 years ago by
Owner: | goldfire deleted |
---|---|
Resolution: | duplicate |
Status: | closed → new |
Unfortunately it looks like the initial implementation of type-indexed Typeable
won't actually address this issue. We'll see what the future holds in store.
comment:37 Changed 3 years ago by
Is this done? comment:35 is a bit cryptic. If not done, could you clarify what remains?
comment:38 Changed 3 years ago by
From the discussion I've seen, I am purely guessing that all the necessary internal representations are now available, but the solver part is not. I.e. with PolyKinds
enabled, the definition
{-# LANGUAGE PolyKinds #-} import Data.Typeable f :: Typeable a => Proxy a -> TypeRep f = typeOf
still won't compile, but you probably can now use the new TypeRep
mechanisms do write an equivalent function by hand.
On the other hand, since 8.0 with TypeInType
you can write
f :: (Typeable (a::k), Typeable k) => Proxy a -> TypeRep f = typeOf
which means the actual need for this improvement is less than it was in 7.10.
At the time I wrote this ticket, I was somewhat thinking about preserving backwards compatibility, which got broken in 7.10 anyhow.
(And until recent trouble with the constraints
package, I thought no one had been affected in practice - but the last version of that package actually now restricts the kind of the Deferrable (a ~ b)
instance to *
in just 7.10, because of this, see discussion at end of https://github.com/ekmett/constraints/issues/43.)
Incidentally in GHCi 8.0.1, with PolyKinds
but not TypeInType
enabled:
Prelude Data.Typeable> let f x@Proxy = typeOf x Prelude Data.Typeable> :t f f :: forall k (t :: k). (Typeable * k, Typeable k t) => Proxy k t -> TypeRep
which is convenient, but means you get an inferred type you cannot write.
comment:39 Changed 3 years ago by
Personally, I am satisfied with the status quo of being able to write,
f :: (Typeable (a::k), Typeable k) => Proxy a -> TypeRep f = typeOf
oerjan, if you also think that this is satisfactory then feel free to close this ticket.
comment:40 Changed 3 years ago by
Resolution: | → wontfix |
---|---|
Status: | new → closed |
Yes, I see that even my "kitchen sink" example can be fixed with a simple Typeable k
constraint. And as in my previous comment, such constraints can be inferred too.
So since I don't know any examples that this doesn't suffice for, I'll close this.
I agree that a
kindRep :: TypeRep -> TypeRep
or perhapskindRep :: Typeable a => proxy a -> TypeRep
is in order. It seems this is useful independent of kind equalities, though it will likely become more useful (and conspicuously missing if unimplemented) with kind equalities.