类型解构

Question

我的数据类型总是至少有两个参数,最后两个参数分别是'q'和'm':

{-# LANGUAGE TypeFamilies, FlexibleContexts, UndecidableInstances, TypeOperators, DataKinds, ConstraintKinds, FlexibleInstances #-}

data D1 q m = D1 q
data D2 t q m = D2 q

class Foo a where -- a has kind * -> *
   f :: a x -> a x

class (Foo b) => Bar b where -- b has kind * -> *
   -- the purpose of g is to change ONE type parameter, while fixing the rest
   -- the intent of the equality constraints is to decompose the parameter b into
   -- its base type and 'q' parameter, then use the same base type with a *different*
   -- `q` parameter for the answer
   g :: (b ~ bBase q1, b' ~ bBase q2) => b m -> b' m

instance (Foo (D2 t q), Integral q) => Bar (D2 t q) where
   g (D2 q) = D2 $ fromIntegral q -- LINE 1

该程序导致错误

Could not deduce (bBase ~ D2 t0) (LINE 1)

当我编写实例时,我当然打算bBase ~ D2 t.我想t不会以某种方式绑定(因此引入了t0),我不知道GHC是否可以解构这种类型.或许我只是在做一些愚蠢的事情.

更重要的是,如果我将参数设置为Bar有类型* - >* - >*,则不需要这种类型的相等/类型解构.但后来我无法强制执行Foo约束:

class (Foo (b q)) => Bar b where -- b has kind * -> * -> *
  g :: b q m -> q b' -- this signature is now quite simple, and I would have no problem implementing it

这不起作用,因为q不是Bar的参数,我不希望它成为Bar的参数.

我找到了一个使用两个额外"虚拟"关联类型的解决方案,但如果我不需要它,我真的不喜欢它们:

class (Foo b, b ~ (BBase b) (BMod b)) => Bar b where -- b has kind * -> *
  type BBase b :: * -> * -> *
  type BMod b :: *

  g :: (Qux (BMod b), Qux q') => b m -> (BBase b) q' m

instance (Foo (D2 t q), Integral q) => Bar (D2 t q) where
  type BBase (D2 t q) = D2 t
  type BMod (D2 t q) = q

  g (D2 q) = D2 $ fromIntegral q

这是有效的,但它相当于明确地解构了类型,我认为在实例的简单类型下应该是不必要的.

我正在寻找任何一种方法的解决方案:要么告诉我如何在"更多应用"类型上强制执行类约束,要么告诉我如何制作GHC解构类型.

谢谢!

Answer 1

根据您的描述，您b' :: * -> * -> *希望限制所应用的类型b' t :: * -> *（对于 all t）。

正如您总结的那样，您要么需要解构一个类型，这是您在这里从b :: * -> *假设为类型应用程序的结果开始的尝试b = b' t，要么对“更多应用”类型强制实施约束，而不是从起点开始的b' :: * -> * -> *.

解构类型是不可能的，因为编译器b甚至不知道是否“可解构”。确实，可能不是，例如，我可以创建一个实例instance Bar Maybe，但Maybe不能解构为一个类型b' :: * -> * -> *和某种类型t :: *。

相反，从 type 开始b' :: * -> * -> *，对应用程序的约束b'可以移至类的主体中，其中变量被量化：

  class Bar (b :: * -> * -> *) where
      g :: (Foo (b q1), Foo (b q2)) => b q1 m -> b q2 m

对于您的示例，还有一个进一步的问题：q1 和 q2 可能有自己的约束，例如，对于D2您需要Integral约束的实例。但是，修复所有实例的Bar约束（在本例中为空约束）。解决方案是使用“constraint-kinded type family”，它允许实例指定自己的约束：q1q2

  class Bar (b :: * -> * -> *) where
      type Constr b t :: Constraint
      g :: (Foo (b q1), Foo (b q2), Constr b q1, Constr b q2) => b q1 m -> b q2 m

（包含{-# LANGUAGE ConstraintKinds #-}并导入GHC.Prim）

然后你可以编写你的D2实例：

   instance Bar (D2 t) where
      type Constr (D2 t) q = Integral q
      g (D2 q) = D2 $ fromIntegral q