Search code examples
haskelltype-familiespolykinds

Is it possible to define variadic-kinded data types?

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?

Solution

  • 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.