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 mniip)

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 mniip

Description: modified (diff)

comment:2 Changed 12 months ago by 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?

comment:3 Changed 12 months ago by RyanGlScott

Keywords: Roles added

comment:4 in reply to:  2 Changed 12 months ago by mniip

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 goldfire

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 Iceland_jack

Cc: Iceland_jack added
Note: See TracTickets for help on using tickets.