类型解构 [英] Type Deconstruction
问题描述
我的数据类型总是至少有两个参数，最后两个参数分别是'q'和'm'：
{ - ＃LANGUAGE TypeFamilies，FlexibleContexts，UndecidableInstances，TypeOperators，DataKinds，ConstraintKinds，FlexibleInstances＃ - }
data D1 qm = D1 q
data D2 tqm = D2 q
类Foo a where - a has kind * - > *
f :: a x - > a x
class（Foo b）=>酒吧b其中 - b有种类* - > *
- g的目的是改变一个类型参数，同时修复其余的
- 等式约束的意图是将参数b分解为
- 它的基类型和'q'参数，然后使用具有*不同* b $ b - `q`参数的相同基本类型作为答案
g ::（b〜bBase q1，b'〜bBase q2）=> ; b m - > b'm
实例（Foo（D2 t q），积分q）=> Bar（D2 tq）其中
g（D2 q）= D2 $ fromIntegral q - LINE 1
< （bBase〜D2 t0）（LINE 1）
<$ p
$ b
这个程序导致错误 / code> 当我编写实例时，我当然希望 bBase〜D2 t 。我想t不会被约束（因此引入了t0），我不知道GHC是否可以解构这种类型。或者我只是在做一些愚蠢的事情。
更重要的是，如果我将参数设置为Bar，这种类型的相等/类型解构就没有必要有善良* - > * - > *。但是，我无法执行Foo约束：
pre code> class（Foo（b q））=>酒吧b其中 - b有种类* - > * - > *
g :: b q m - > q b' - 这个签名现在很简单，而且我没有执行它的问题
将不会工作，因为q不是bar的参数，而且我也不希望将它添加到Bar的参数中。
我找到了一个解决方案使用两个额外的虚拟关联类型，但我真的不喜欢让他们在周围，如果我不需要他们：
<$ c （foo b，b〜（BBase b）（BMod b））=>酒吧b其中 - b有种类* - > *
类型BBase b :: * - > * - > *
型BMod b :: *
g ::（Qux（BMod b），Qux q'）=> b m - > （BBase b）q'm
instance（Foo（D2 t q），积分q）=> Bar（D2 tq）其中
类型BBase（D2 tq）= D2 t
类型BMod（D2 tq）= q
$ b $（D2 q）= D2 $从一元q
这有效，但它等于明确地解构类型，我认为这是不必要的，
我正在寻找两种方法的解决方案：告诉我如何对更多应用类型强制执行类约束，或告诉我如何让GHC解构类型。
谢谢！
根据你所描述的，你有类型 b':: * - > * - > * 您希望限制所应用的 b't :: * - > * （所有 t ）。
在你总结的时候，你需要解构一个类型，这是你在这里尝试
从 b :: * > * 假定是
类型应用程序的结果 b = b't ，或者对more-应用类型，而不是从 b':: * - >的起点。
。 * - > *
解构类型是不可能的，因为编译器不知道 b 实例Bar Maybe ，但是 Maybe 不能被解构成类型 b':: * - > * - > * 和某些类型 t :: * 。
从类型 b':: * - > * - > * ，对 b'的应用程序的约束可以移动到类的主体中，在该类中量化变量：
class Bar（b :: * - > * - > *）其中
g ::（Foo（b q1）， Foo（b q2））=> b q1 m - > b q2 m
对于您的示例，还有一个折痕：q1和q2可能有自己的约束，
例如对于 D2 实例，您需要 Integral 约束。但是， Bar 修复了 q1 和 q2 的约束。所有实例（在本例中为空约束）。一个解决方案是使用限制类型的家庭，它允许实例指定自己的约束：
class Bar（b： ：* - > * - > *）其中
类型Constr bt ::约束
g ::（Foo（b q1），Foo（b q2），Constr b q1，Constr b q2）= > b q1 m - > （包括 { - ＃LANGUAGE ConstraintKinds＃ - } $ b $ / code> code>并导入 GHC.Prim ）
D2 实例： 实例Bar（D2 t）其中
类型Constr（D2 t ）q =积分q
g（D2 q）= D2 $ fromInteral q
My data types will always have at least two parameters, and the last two parameters are always 'q' and 'm', respectively:
{-# 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
This program results in the error
Could not deduce (bBase ~ D2 t0) (LINE 1)
When I wrote the instance, I certainly intended bBase ~ D2 t. I guess t is not bound somehow (hence the introduction of t0), and I don't know if GHC can deconstruct this type at all. Or maybe I'm just doing something silly.
More to the point, this kind of type equality/type deconstruction wouldn't be necessary if I make the parameter to Bar have kind * -> * -> *. But then I couldn't enforce the Foo constraint:
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
This won't work because q is not a parameter to Bar, and I don't want it to a parameter to Bar.
I found a solution using TWO extra "dummy" associated types, but I don't really like having them around if I don't need them:
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
This works, but it amounts to explicitly deconstructing the type, which I think should be unnecessary given the simple type of the instance.
I'm looking for a solution to either approach: either tell me how I can enforce a class constraint on a "more-applied" type, or tell me how to make GHC deconstruct types.
Thanks!
From what you describe, you have types b' :: * -> * -> * for which you wish to constrain the applied b' t :: * -> * (for 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
这篇关于类型解构的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
