Opened 12 months ago
Last modified 12 months ago
#15707 new feature request
More liberally kinded coercions for newtypes
Reported by: | mniip | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.6.1 |
Component: | Compiler (Type checker) | Version: | 8.6.1 |
Keywords: | Roles | Cc: | Iceland_jack |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | #12369 | Differential Rev(s): | |
Wiki Page: |
Description (last modified by )
Consider the infinite data family (possible thanks to #12369):
data family I :: k -> k newtype instance I a = I0 (a) newtype instance I a x = I1 (a x) newtype instance I a x y = I2 (a x y) newtype instance I a x y z = I3 (a x y z) ...
We end up with a family of eta-contracted coercions:
forall (a :: *). a ~R I a forall (a :: k -> *). a ~R I a forall (a :: k -> l -> *). a ~R I a forall (a :: k -> l -> m -> *). a ~R I a ...
What if we could somehow indicate that we desire a polykinded newtype (so to speak) with a coercion forall (a :: k). a ~R I a
Maybe even do so by default: newtype I a = I0 a
would create such a polykinded coercion. Though the I0
data constructor and pattern would still only use the *-kinded restriction of it.
We could then recover other constructors with:
i1 :: a x -> I a x i1 = coerce ...
Change History (6)
comment:1 Changed 12 months ago by
Description: | modified (diff) |
---|
comment:2 follow-up: 4 Changed 12 months ago by
comment:3 Changed 12 months ago by
Keywords: | Roles added |
---|
comment:4 Changed 12 months ago by
Replying to goldfire:
I see where you're getting, but it's still wishy-washy to me. Is there a concrete program you'd like to write with this feature?
Me (and partly ekmett) are experimenting with the idea of building a polykinded generics framework using a type-level combinatory calculus. So there's a handful of such data families involved, acting as combinators.
In practice of course the family can't be infinite and we have to stop at some arity. We could unsafely introduce a coercion of the desired shape, but then what if someone extends the family?
comment:5 Changed 12 months ago by
But do you have a concrete program (invent syntax if necessary) that uses this feature? It's much easier to understand the implications of it all with an example.
comment:6 Changed 12 months ago by
Cc: | Iceland_jack added |
---|
I see where you're getting, but it's still wishy-washy to me. Is there a concrete program you'd like to write with this feature?