代码之家 › 专栏 › 技术社区 › luqui

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

polykinds type-families haskell

1

luqui · 技术社区 · 6 年前

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

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,

还有其他的窍门吗?

1 回复 | 直到 6 年前

1

2

luqui 6 年前

“公理化”方法确实有效,我刚才用的等式是错误的:

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 必须通知类型检查器在何处应用公理。我做的 a full development 以供参考。

注意,当我玩这个的时候,我有一次得到了GHC恐慌。所以恶作剧可能是恶作剧。仍然对其他方法感兴趣。