- 
                Notifications
    You must be signed in to change notification settings 
- Fork 1.1k
Description
As suggested by @abgruszecki in #7389, we should investigate adding a primitive match type to lift * -> *-kinded operators to arbitrary kinds.
Instead of creating special
HeadPKandTailPKprimitive match types (HeadandTailfrom Miles' post above), I think it > would be feasible to instead have aLiftPKprimitive (lift poly-kinded)
which allows lifting any type operator of kind* -> *to operate on types of arbitrary kinds, and thus allows definingHeadPKandTailPK. The benefit is thatLiftPKallows making all type operators poly-kinded, instead of special-casingHeadandTail, and doesn't seem significantly harder to define. It would behave as follows:
type LiftPK[[]] = ... // compiler-provided
type HeadPK[t] = LiftPK[Head][t] // consistent behaviour with Miles' Head
Head[(1,2,3)] === 1
HeadPK[(1,2,3)] === 1
HeadPK[[t] => (t, 2, 3)]] === [t] => t
type TailPK[t] = LiftPK[Tail][t] // similarly, has behaviour consistent with Tail from the preceding post
As for compiler implementation (and probably as a reminer for @OlivierBlanvillain),
LiftPKshould be implementable by inventing an abstract type for each type parameter, replacing type parameter references with those types, reducing match type (if there's any to be reduced) and undoing the type parameter substitution.