Opened 11 months ago

Last modified 11 months ago

#9429 new feature request

Alternative to type family Any

Reported by: mboes Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.9
Keywords: Cc: facundo.dominguez, m@…, edsko, ekmett, rrnewton, GregoryCollins
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: 9097, 9380 Differential Revisions:

Description (last modified by mboes)

In GHC HEAD, Any is no longer a datatype. There are good reasons for this change, one of which was explained in #9097, the original ticket, and another in #9380. Unfortunately, a casualty of this change is that it is no longer easy to generalize the rank1dynamic package to rank-1 types with type variables of arbitrary kind (not just *). We submitted a way to do so here, that exploits the fact that Any has the very magical property of inhabiting *all* kinds, including closed ones.

This works for GHC 7.8, but won't work in HEAD, because we require that there exists a Typeable instance for Any, just as there are Typeable instances for any other type one wishes to have instances for. The reason is that now that Any is a type family, Any is no longer a legal instance head.

There are several possible solutions that I see:

  • while it's clearly dangerous for the compiler to be inserting the old Any during typechecking from the moment that we have computation in types over closed kinds, we may still want the old Any, say under a different name, as a backdoor. It wouldn't be used by the compiler during type checking - only by packages such as rank1dynamic. I believe that furthermore, if we restrict the old Any to not inhabit closed kinds, then none of the problems cited in the above tickets arise.
  • Instead of making the new Any a type family, keep it a datatype, but ban it from inhabiting closed kinds. I don't know if such an Any would be sufficient for the purposes of GHC, however.
  • Hardwire a Typeable instance for the Any type family (not sure if this makes sense).

Change History (29)

comment:1 Changed 11 months ago by mboes

  • Description modified (diff)

comment:2 Changed 11 months ago by mboes

  • Description modified (diff)

comment:3 Changed 11 months ago by mboes

Fixed link to rank1dynamic pull request: https://github.com/haskell-distributed/rank1dynamic/pull/6

comment:4 Changed 11 months ago by edsko

  • Cc edsko added

comment:5 Changed 11 months ago by mboes

Hm, perhaps I was a bit too hasty about the "inhabiting only open kinds" criterion as being sufficient for safety. In #9380, we have a GADT indexed by types in a closed kind. But the breaking test case exposed there would break just as well with an open kind, I think. The problem is that GHC chooses Any as an arbitrary instantiation for some unbound type variable appearing in the type index of the GADT, which then leads GHC to wrongly identify some alternatives as being "unreachable" in case analyses. Therefore, the second solution in the description of this ticket would still have problems with GADT's.

I guess my point is that while the Any that GHC uses to silently instantiate things during type checking should be well behaved, clearly, there could be an UnsafeAny, similar to the old Any, for certain targeted use cases such as obtaining the TypeRep of a polymorphic type with no type families. For polymorphic types where there might be occurrences of type families, I so no other solution but to somehow make the Any-the-type-family Typeable somehow.

comment:6 Changed 11 months ago by facundo.dominguez

  • Cc facundo.dominguez added; facundo.dominguez@… removed

comment:7 Changed 11 months ago by goldfire

While #9380 is indeed fixed by making Any a type family, an alternative fix would be to change the pattern-match pruner to be Any-aware. I say this because there is something sensible about allowing Any to be a datatype in any open kind. I haven't quite thought it all through, but somehow that might make sense.

comment:8 Changed 11 months ago by carter

Is something like Any needed, or just a way of reifying that polymorphic type? (i'm trying to understand what the fundamental problem is vs whats currently needed to solve the problem)

comment:9 Changed 11 months ago by mboes

Making pattern-matching Any-aware makes sense to me. Again, I'm not qualified to understand what the best way forward is here. But to answer carter's question, ultimately for the purposes of rank1dynamic (and by extension Cloud Haskell), what we need is way of reifying more polymorphic types than we currently can.

Introducing some kind of PolyTypeable mechanism could certainly bypass the question at hand. Really not sure how such an extension would work though.

comment:10 follow-up: Changed 11 months ago by carter

ok, now if we had a hypothetical PolyTypeable would you have other remaining needs for Any?

It occurs to me as I'm saying this, that to some extent PolyTypeable is possible today via data/newtype wrapping a polymorphic type! For you use case, Is that a viable solution today (aesthetics aside) or is there a fundamental barrier to that being suitable?

comment:11 Changed 11 months ago by ekmett

  • Cc ekmett added

comment:12 in reply to: ↑ 10 Changed 11 months ago by mboes

Replying to carter:

ok, now if we had a hypothetical PolyTypeable would you have other remaining needs for Any?

I myself wouldn't. I don't know of other use cases beyond the ones internal to GHC.

It occurs to me as I'm saying this, that to some extent PolyTypeable is possible today via data/newtype wrapping a polymorphic type! For you use case, Is that a viable solution today (aesthetics aside) or is there a fundamental barrier to that being suitable?

Interesting idea. But I'm afraid it isn't a solution without its problems, beyond the mere verbosity that it might induce.

If I understand your idea correctly, you're saying that if you want to send say bind, then you introduce the following type and wrap bind:

data Dict c = c => Dict
newtype BindWrap = BindWrap (forall a m. Dict (Monad m) -> m a -> (a -> m b) -> m b)
bindWrap = BindWrap $ \Dict -> (>>=)

Now, you can send a label for bindWrap to the remote side, along with the TypeRep for BindWrap.
But you can't compose bindWrap. That is, bindWrap is a "static value" in the sense that it doesn't depend on any other runtime "dynamic" value. In other words, it has no free variables. If we say that labels for static values x :: a have type Static a, then I can't combine bindWrap with say action :: Static [Int] using

staticApply :: Static (a -> b) -> Static a -> Static b

because bindWrap is of atomic type. The only reasonable type that I can give to any label for it is Static BindWrap. But that's not a Static with an arrow type index.

So while you can send bindWrap, you can't send compositions of it with other Static things. This is an important feature for many Cloud Haskell use cases.

comment:13 Changed 11 months ago by rrnewton

Hi all,

Uh oh! Our approach to lock-free data structures in Haskell (atomic-primops, chaselev-deque, lockfree-queue, concurrent-skiplist) is based on Any.

The way we use Any is simply to prevent GHC from performing any optimizations that change the pointer identity of the object. That is, the "Ticket" type in atomic-primops is really just an Any. Is there some other way to accomplish this goal via other means in GHC head? Perhaps we need something like NOINLINE...

Johan's been adding more and better atomic memory primop support in HEAD but it sounds like this is at cross purposes with Any also being removed from HEAD!

Last edited 11 months ago by rrnewton (previous) (diff)

comment:14 Changed 11 months ago by rrnewton

  • Cc rrnewton added

comment:15 Changed 11 months ago by tibbe

There's another use of Any that I'm aware of that might not work anymore, to create unique tombstone values that can be compare using reallyUnsafePtrEquality#. See e.g. https://github.com/gregorycollins/hashtables/blob/8a1ed23450377360e4b53b83c531f7557fff7e79/src/Data/HashTable/Internal/UnsafeTricks.hs#L38. These tricks allow you to write a Maybe a represents null values (or any number of unary constructors) using a designated pointer instead of an indirection.

comment:16 Changed 11 months ago by tibbe

  • Cc GregoryCollins added

comment:17 Changed 11 months ago by goldfire

It's not clear to me that Ryan's and Johan's uses are in conflict with the Any change. Any is still around and still usable in HEAD. It just can't appear in a type pattern -- that is, on the LHS of a type family equation or in an instance head. Is Any used in this way in the programs cited above? In particular, it assuredly is still possible to cast to Any and then cast back.

comment:18 Changed 11 months ago by rrnewton

Oh, there may be no problem then. I misread and thought Any was gone in its previous form. I'll test it and try to get our packages working on GHC head.

comment:19 Changed 11 months ago by simonpj

I'm a bit lost in this thread. As Richard says (comment:17),

  • Any is still a valid type that can inhabit any kind
  • but you can't pattern-match on it in an instance declaration

There are good reasons for this design. One that has not been mentioned so far is #7259: eta expansion of products. Admittedly we don't have this now, but in some sense we should have, and I'd be reluctant to move to a design that precluded it.

If there is still a lack, could someone articulate just what it is, preferably explicitly (articulating problem, solution) rather than by saying that rank1dyanamic doesn't work.

comment:20 Changed 11 months ago by mboes

Problem: as mentioned in the description, Any-the-type-family does not admit a Typeable instance. Any-the-datatype does. We need a Typeable instance because Any is used as a proxy for type variables when invoking typeOf on a value at a polymorphic type.

Context: rank1dynamic generalizes Data.Typeable to handle rank-1 polymorphic types, not just monotypes. This is useful because in Cloud Haskell one often expects a polymorphic function to be received. Any incoming function must be tagged with a representation of its type in order to compare it the expected type. rank1dynamic currently only handles types with quantified type variables of kind *. To make it handle types with quantified type variables of arbitrary kind, we instantiate all type variables with Any in order to get a monotype, for which we can get a typeOf can give us a runtime representation. Example:

data Dict c = c => Dict
return' :: Dict (Monad m) -> a -> m a
type ANY1 = Any
type ANY2 = Any Any

tyreturn' = typeOf (return' :: Dict (Monad ANY1) -> ANY2) 

this only works if Any has a Typeable instance. Otherwise, the Typeable constraint for the type written down in the signature cannot be satisfied.

Possible solutions:

  1. Hardcode a Typeable instance for Any in GHC, even though it is now a type family.
  2. Reintroduce a new Any-the-datatype in the compiler, under a different name, and use that in rank1dynamic instead of GHC HEAD's Any-the-type-family. Restrict this Any-the-datatype to inhabit only open kinds, not closed kinds, in order to avoid #9380, #9097.
  3. Same as previous solution, but don't bother with any restrictions on what kinds are inhabited. Consider this new Any-the-datatype *really-unsafe-use-at-your-own-risks*. Its use in rank1dynamic would be fine for types with no occurrences of closed type families. It would not work ok for more exotic types, but I don't think that would be a big deal in practice.

comment:21 follow-up: Changed 11 months ago by carter

or 4. come up with an alternative way to support Typeable instances on polymorphic values? right?

comment:22 in reply to: ↑ 21 Changed 11 months ago by mboes

Replying to carter:

or 4. come up with an alternative way to support Typeable instances on polymorphic values? right?

Yes, absolutely. No idea how to articulate that solution further though.

comment:23 Changed 11 months ago by simonpj

I'm sorry, but I still don't understand the problem.

  • Why exactly do you need a Typeable instance for types involving GHC's built-in Any?
  • In the example you give in "Context", you could perfectly well declare your own data type MyAny and use it instead of Any.

To be concrete, can you give a more complete example that shows why it's essential to have a Typeable instance for GHC's Any?

Thanks

Simon

Last edited 11 months ago by simonpj (previous) (diff)

comment:24 Changed 11 months ago by goldfire

But MyAny's kind must end in -> *. This would limit the ability of poly-kinded higher-rank functions in Cloud Haskell, no?

comment:25 Changed 11 months ago by mboes

  • If I declare MyAny, then as goldfire pointed out, it can only have a kind of the form -> *. As it is, if rank1dynamic uses a datatype of fixed kind, as for MyAny, then I will need many, many of those datatypes, defined a priori. To handle multiple type variables, as in the example given previously, I need a family MyAny1, MyAny2, MyAny3, etc... Along an orthogonal dimension, to handle multiple kinds, I will need multiple MyAnys, i.e. MyAny1_s, MyAny1_ss, MyAny2_s, MyAny2_ss, etc (where MyAny_s is of kind *, MyAny_ss is o f kind * -> *, etc). And even with that proliferation of datatypes, I still wouldn't be able to handle type variables of user-defined kind, or even of Constraint kind.

The beauty of the Any type in this use case is that because it inhabits all kinds, I can use Any to instantiate the first type variable, Any Any to instantiate the second, Any Any Any to instantiate the third, etc. Moreover, I can still use those no matter the kinds of the type variables. I only need a single datatype, to serve as a proxy for an arbitrary number of type variables, each of arbitrary kind.

  • A larger end-to-end example will take a little while to write, but I'll try to do so tonight. At this point, if it can clarify things, let's just say that any message that gets sent over the wire needs an accompanying TypeRep of its type in order for the receiver to make sense of the payload. Sometimes the payload is a function, and sometimes that function is polymorphic and can be called by the receiver at any argument type. We can't represent polymorphic types directly, so for a function of type forall a. a -> a, we send the TypeRep for Any -> Any instead.

comment:26 Changed 11 months ago by ekmett

Note: you already have multiple "MyAnys" Any inhabits all kinds, so Any :: Nat -> * is also a perfectly cromulent type it can inhabit, allowing you to use Any 0, Any 1, Any 2...

This means having Any doesn't just punch a "one extra distinguishable member of every kind" sized hole in the sanity of the typesystem but rather it creates an infinite family of such holes.

I abused that for a while in Hask to create 'evil' targets for compositions of functors to other kinds, etc. but the status quo comes at a terrible terrible price. We can no longer reason that a closed kind has a fixed set of inhabitants.

Bool is currently inhabited by True, False, and Any 'FileNotFound as distinguishable inhabitants along with an infinite set of other such exotic beasts.

This implementation strategy is also very leaky. You have to be very careful, as it is possible to subvert the use of this sort of mechanism very easily (and accidentally) in the presence of functional dependencies when you go to apply it in situations where one of the arguments is a GADT or functional dependency, argument to a class, etc. This can lead to straight up segfaults, not just local type strangeness.

comment:27 Changed 11 months ago by simonpj

If the issue is getting a type rep for a polymorphic type, let's address that problem directly, rather than hack a solution (by representing forall a. a->a as Any -> Any) in which the hack itself has pervasive negative consequences.

See also #7015, where this same issue arises.

Simon

comment:28 Changed 11 months ago by mboes

To be clear, as I have said before, I'm not arguing for reverting back to the status quo that we have in GHC 7.8. It's pretty clear that we want to avoid having (an infinite number of) exotic inhabitants of kinds that are intended to be closed (and often with a finite number of inhabitants).

As I see it if the old Any-as-datatype is revived under a different name, without imposing any restrictions on what kinds it inhabits (i.e. only open kinds), it would have to be in an Unsafe.* module, and only brought in scope in some very clearly delineated modules. At least in the case of Cloud Haskell, there is no reason why the user needs to even know of its existence - it's use can be contained, "behind the scenes". That may well still be unsatisfactory.

simonpj: I'm all for a better solution that is not a hack like rank1dynamic is, but do you have any ideas for how generating TypeReps for polymorphic types might work? rank1dynamic has the merit of existing today, and the reason we're seeking to extend it is precisely to help with #7015 without having to rewrite some of the internals of distributed-process. Of course, if we do understand how to get type reps for polymorphic types, Facundo and I are happy to volunteer some time to do the rewriting.

So again, there are 4 possible solutions here. I don't know which one would be best, but it would be nice to support a better story for Cloud Haskell, which already has a number of users, while still keeping to a minimal impact on the compiler.

comment:29 Changed 11 months ago by simonpj

See discussion in #7015

Note: See TracTickets for help on using tickets.