是否可以定义可变种类的数据类型?

Question

我可以像这样定义一个多种类的自然变换：

type family (~>) :: k -> k -> *
type instance (~>) = (->)
newtype NT a b = NT { apply :: forall x. a x ~> b x }
type instance (~>) = NT

它适用于各种类型，所以我可以定义例如

left :: Either ~> (,)
left = NT (NT (Left . fst))

这很酷，也很鼓舞人心。 但是无论我玩多少花样，我似乎都无法在返回类型中得到一些可变参数。 例如，我想要

type family (:*:) :: k -> k -> k
type instance (:*:) = (,)
type instance (:*:) = ???

这似乎是不可能的，因为类型族需要完全饱和，并且只能在*中引入类型构造函数。

我什至尝试了一些相当讨厌的技巧

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)

我不知道这是否有任何希望起作用，因为我还没有想过如何"代表"更高层次的东西。 但GHC知道我在撒谎

• Couldn't match type ‘(,)’ with ‘Promote2 (,) a’
Inaccessible code in
a pattern with constructor: Refl :: forall k (a :: k). a :~: a,

还有其他技巧吗？

Answer 1

"公理化"方法确实有效，我只是错误地使用了相等式：

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

使用Equality.apply对于通知类型检查器在哪里应用公理至关重要。 我在这里对高等产品进行了全面开发，以供参考。

请注意，当我玩这个时，我有一次 GHC 恐慌。 所以讨厌的伎俩可能是讨厌的。 仍然对其他方法感兴趣。