1

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

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,

有没有其他技巧呢？

4

1 回答 1

2

“公理”方法确实有效，我刚刚使用了错误的相等性：

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 恐慌。所以讨厌的把戏可能是讨厌的。仍然对其他方法感兴趣。

于 2018-09-11T06:27:12.523 回答