类型家族情况下的级别约束
Data.Param.FSVec参数化数据有可能具有类型同义词族吗？
理想情况下，我希望这样编译：
class A e where
type Arg e a
f :: (Arg e a -> b) -> e a -> e b
instance A X where
type Arg X a = Nat size => FSVec size a
f = {- implementation -}
我已经尝试了几种解决方法，比如在新类型中包装FSVec size a或约束同义词，但似乎我无法获得任何合理的权利。
上下文+最小工作示例
A是先前定义的类（例如）：
class OldA e where
f :: (Maybe a -> b) -> [e (Maybe a)] -> [e b]
继承OldA的类型的一个例子是：
data Y a = Y a
instance Functor Y where
fmap f (Y a) = Y (f a)
instance OldA Y where
f = fmap . fmap
我想扩展这个类，以便能够为f表示更一般的函数参数。 假设我们有一个类型X和一个相关函数fIndependent ：
import qualified Data.Param.FSVec as V
import Data.TypeLevel hiding ((==))
data X a = X a deriving Show
fromX (X a) = a
fIndependent :: (Nat size) => (V.FSVec size (Maybe a) -> b) -> [X (Maybe a)] -> [X b]
fIndependent _ [] = []
fIndependent f xs = let x' = (V.reallyUnsafeVector . take c . fmap fromX) xs
xs' = drop c xs
c = V.length x'
in if c == length (V.fromVector x') then X (f x') : fIndependent f xs' else []
fIndependent本身就是理智。 用函数测试它
test :: V.FSVec D2 x -> Int
test a = V.length a
将授予结果：
>>> fIndependent test $ map (X . Just) [1,2,3,4,5,6,7,8,9]
[X 2, X 2, X 2, X 2]
好的，现在如何扩展OldA ？ 我想到的最“自然”的东西是为A类装备一个类型同义词族Arg ea ，如下所示。
class NewA e where
type Arg e a
f :: (Arg e a -> b) -> [e (Maybe a)] -> [e b]
转换所有现有的实例很简单：
instance NewA Y where
type Arg Y a = Maybe a
f = fmap . fmap -- old implementation
为了表达fIndependent ，f是困难的部分，因为只是增加
instance NewA X where
type Arg X a = (Nat size) => FSVec size (Maybe a) -- wrong!!!
f = {- same as fIndependent -}
不起作用。 这是我遇到的麻烦。
试奏
大多数解决方案只见提出包装FSVec一个内部newtype 。 这样做并没有帮助，因为下面的代码：
{-# LANGUAGE RankNTypes #-}
newtype ArgV a = ArgV (forall rate.Nat rate => V.FSVec rate (Maybe a))
instance NewA X where
type Arg X a = ArgV a
g f xs = let x' = (V.reallyUnsafeVector . take c . fmap fromX) xs
xs' = drop c xs
c = V.length x'
in if c == length (V.fromVector x') then X (f $ ArgV x') : g f xs' else []
类型推断系统似乎失去了关于size的信息：
Couldn't match type ‘s0’ with ‘rate’ …
because type variable ‘rate’ would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context: Nat rate => V.FSVec rate (Maybe a)
Expected type: V.FSVec rate (Maybe a)
Actual type: V.FSVec s0 (Maybe a)
Relevant bindings include
x' :: V.FSVec s0 (Maybe a)
(bound at ...)
In the first argument of ‘Args’, namely ‘x'’
In the second argument of ‘($)’, namely ‘Args x'’
Compilation failed.
我很感谢在这件事上的任何牵头或暗示。
看来你正在使用一个类Nat :: k -> Constraint和一个数据类型FSVec :: k -> * -> * 。 数据类型受到旧的DatatypeContexts扩展的限制。
{-# LANGUAGE DatatypeContexts #-}
class Nat n
data Nat n => FSVec n a = FSVec -- ...
你有一个现有的A :: (* -> *) -> Constraint ，你想写一个FSVec实例。
class A e where
--- ...
f :: ( {- ... -} b) -> e a -> e b
但FSVec永远不会有A实例，因为它是一种不匹配。 类A需要类型参数* -> *但FSVec有类型k -> * -> * 。 你已经遇到了一个问题，甚至还没有使用类型系列。 如果你试图做到这一点（现在摆脱现在的类型家庭观点）
data X = X
instance A (FSVec) where
type Arg FSVec a = X
f = undefined
你得到一个编译器错误。
Expecting one more argument to `FSVec'
The first argument of `A' should have kind `* -> *',
but `FSVec' has kind `* -> * -> *'
In the instance declaration for `A (FSVec)'
在此之前的所有内容，包括编译器错误，都是传达您遇到的问题的有用信息，对于寻求帮助非常有用。
幸运的是，这是一个很容易解决的问题。 如果你选择一些自然数n ，那么FSVec n有* -> * ，它与A的类型参数类型相匹配。 您可以开始编写instance A (FSVec n)
instance A (FSVec n) where
f = -- ...
当您重新提供类型族的完整类定义时
{-# LANGUAGE TypeFamilies #-}
class A e where
type Arg e a
f :: (Arg e a -> b) -> e a -> e b
该解决方案仍然是写一个A实例FSVec n而不是为FSVec 。 现在n已经进入instance声明中，有一个明显的地方可以捕获所需的Nat n上下文。
instance Nat n => A (FSVec n) where
type Arg (FSVec n) a = FSVec n a
f = undefined -- ...
Cirdec的答案解释了其中一个问题，但是它给出的解决方案并不能完全回答所发布的问题。 该问题要求为类A的实例X提供FSVec类型同义词。
这里的主要问题是防止定义type Arg X = FSVec size a （在任何可能的配置中）是类型族不是内射的。 了解这一点，并遵循Cirdec的推理，我可以想出一个解决方案来实现这一目标：在X类型中包含一个代理“上下文”变量，以克服上述问题。
data X c a = X a
instance (Nat n) => A (X n) where
type (X n) a = FSVec n a
f = {- same as fIndependent -}
当然，这是一个快速修复，适用于最小的示例（即它回答了发布的问题），但在编写f这样的多个函数时可能无法很好地扩展，因为在推断的“上下文”之间可能会出现类型冲突。
我能想到的最佳解决方案是为每个实例添加约束同义词（如此答案所示），如下所示：
import qualified Data.Param.FSVec
import Data.TypeLevel
import GHC.Exts -- for Constraint kind
class A e where
type Arg e context a
type Ctx e context :: Constraint
f :: (Ctx e context) => (Arg e context a -> b) -> [e (Maybe a)] -> [e b]
instance A Y where
type Arg Y c a = Maybe a
type Ctx Y c = ()
f = {- same as before -}
instance A X where
type Arg X size a = V.FSVec size (Maybe a)
type Ctx X size = Nat rate
f = {- same as fIndependent -}
但是，那么我们将不得不处理由于类型家族的臭名昭着的非注入性而导致的模糊类型（例如， Could not deduce: Arg e context0 a ~ Arg e context a ）。 在这种情况下，必须使用GHC 8.0中提供的TypeFamilyDependencies扩展（基于内射类型族）手动完成验证，并将Arg定义为：
type family Arg (e :: * -> *) context = (r :: * -> *) | r -> context
当然，如果类型族的设计不是内射的（这是我的情况），这是不可能的，但它是目前为止最干净的解决方案。 如果可以使用提供的论文中的指导方针来设计她的类型家庭，那么这是绝对推荐的。
链接地址: http://www.djcxy.com/p/66629.html