7

我的数据类型总是至少有两个参数，最后两个参数总是'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 解构类型。

谢谢！

4

1 回答 1

1

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

As you summise, you either need to deconstruct a type, which is your attempt here starting from a b :: * -> * assumed to be the result of a type application b = b' t, or to enforce a constraint on a "more-applied" type, instead from the start-point of a b' :: * -> * -> *.

Deconstructing a type is not possible, since the compiler does not know if b is even "deconstructable". Indeed, it may not be, e.g., I can make an instance instance Bar Maybe, but Maybe cannot be deconstructed into a type b' :: * -> * -> * and some type t :: *.

Starting instead from a type b' :: * -> * -> *, the constraints on an application of b' can be moved into the body of the class, where the variables are quantified:

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

For your example there is one further wrinkle: q1 and q2 may have their own constraints, e.g. for the D2 instance you require the Integral constraint. However, Bar fixes the constraints on q1 and q2 for all instances (in this case the empty constraint). A solution is to use "constraint-kinded type families" which allow instances to specify their own constraints:

  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

(include {-# LANGUAGE ConstraintKinds #-} and import GHC.Prim)

Then you can write your D2 instance:

   instance Bar (D2 t) where
      type Constr (D2 t) q = Integral q
      g (D2 q) = D2 $ fromIntegral q
于 2013-01-30T13:45:22.697 回答