I can define a polykinded natural transformation like so:
type family (~>) :: k -> k -> *
type instance (~>) = (->)
newtype NT a b = NT { apply :: forall x. a x ~> b x }
type instance (~>) = NT
Which works at all kinds, so I can define e.g.
left :: Either ~> (,)
left = NT (NT (Left . fst))
This is cool and inspiring. But no matter how many tricks I play, I can't seem to get something variadic in the return type. E.g. I would like
type family (:*:) :: k -> k -> k
type instance (:*:) = (,)
type instance (:*:) = ???
It seems like this is impossible, since type families need to be fully saturated, and you can only introduce type constructors in *
.
I've even tried some rather nasty tricks
type instance (:*:) = Promote2 (:*:)
type family Promote2 :: (j -> k -> l) -> (a -> j) -> (a -> k) -> (a -> l) where
promote2_law :: Promote2 f x y z :~: f (x z) (y z)
promote2_law = unsafeCoerce Refl
fstP :: forall (a :: k -> *) (b :: k -> *) (c :: k). (a :*: b) c -> a c
fstP = case promote2_law @(:~:) @a @b @c of Refl -> NT (\(a,b) -> a)
And I don't know if that even has any hope of working, since I haven't thought through how higher kinded things are "represented". But GHC knows I'm lying anyway
• Couldn't match type ‘(,)’ with ‘Promote2 (,) a’
Inaccessible code in
a pattern with constructor: Refl :: forall k (a :: k). a :~: a,
Are there any other tricks for this?
The "axiomatic" approach does actually work, I had just used the equality wrong:
fstP :: forall (a :: j -> k) (b :: j -> k) (x :: j). (a :*: b) x -> a x
fstP = castWith (Refl ~% promote2_law @(:*:) @a @b @x ~% Refl) fst
where
infixl 9 ~%
(~%) = Data.Type.Equality.apply
Using Equality.apply
is essential to inform the type checker of where to apply the axiom. I made a full development of higher-kinded products here for reference.
Be warned, as I was playing with this did I get a GHC panic once. So the nasty tricks might be nasty. Still interested in other approaches.