类型解构

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的参数设置为* - > * - > *，那么这种类型的类型/类型解构就没有必要了。但我不能强制约束富：

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是不是酒吧的参数，我不希望它的参数吧。

我发现使用两个额外的“虚拟”相关类型的解决方案，但我真的不喜欢让他们身边，如果我不需要他们：

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 :: * -> *（所有t）。

当你summise，你要么需要解构一个类型，它是你的企图在这里 从b :: * -> *开始认为是一种 应用b = b' t，或执行一个“更适用”约束的结果从b' :: * -> * -> *的起点改为 。

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

从类型b' :: * -> * -> *代替开始，对b'应用程序中的约束可被移入类的主体，其中变量被量化：

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

对于示例有一个另外的皱纹： q1和q2可能有自己的限制，例如 对于D2实例，您需要约束Integral。但是，Bar修复了所有实例的q1和q2的约束（在本例中为空约束）。一种解决方法是使用“约束的kinded型家庭”，让实例来指定自己的约束：

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