Opened 3 years ago

Last modified 3 years ago

#12766 new feature request

Allow runtime-representation polymorphic data families

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: TypeInType Cc:
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 Iceland_jack)

This is an offshoot of #12369 (‘data families shouldn't be required to have return kind *, data instances should’), allowing family declarations something like:

data family Array a :: TYPE rep

Change History (2)

comment:1 Changed 3 years ago by Iceland_jack

Description: modified (diff)

comment:2 Changed 3 years ago by Iceland_jack

Explore how ticket:12369#comment:3, ticket:12369#comment:4 fit into this.

TODO How Free fits with Levity-Polymorphic Type Classes, can we define something like this

newtype instance Free (k :: TYPE rep -> Constraint) (p :: TYPE rep) :: TYPE rep where
  Free0 :: (forall q. k q => (p -> q) -> q) -> Free k p

TODO or like this

newtype instance Fix (f :: TYPE rep -> TYPE rep) :: TYPE rep where
  In :: f (Fix f) -> Fix f

And would they be useful

TODO Look at Ran and Lan and their hierarchies.

Last edited 3 years ago by Iceland_jack (previous) (diff)
Note: See TracTickets for help on using tickets.