类型族实例中的类型级约束

Question

是否可以为参数化数据（例如 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 之前定义的（例如）这样的：

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

我想扩展这个 class 以便能够为 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？我想到的最多 "natural" 的事情是为 class A 配备一个类型同义词族 Arg e a 如下。

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.

对于此事的任何线索或提示，我将不胜感激。

Answer 1

您似乎正在使用 class Nat :: k -> Constraint 和数据类型 FSVec :: k -> * -> *。数据类型受限于旧的 DatatypeContexts 扩展名。

{-# LANGUAGE DatatypeContexts #-}

class Nat n

data Nat n => FSVec n a = FSVec -- ...

您有一个现有的 class A :: (* -> *) -> Constraint，您想为其编写一个 FSVec 实例。

class A e where
  --- ...
  f :: ( {- ... -} b) -> e a -> e b

但是 FSVec 永远不会有 A 实例，因为这是一种不匹配。 class A 需要类型参数 * -> * 但 FSVec 具有类型 k -> * -> *。您已经运行遇到了问题，甚至还没有使用类型族。如果你尝试这样做（暂时放弃 type family 参数）

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 = -- ...

当您重新引入具有类型 family

的完整 class 定义时

{-# LANGUAGE TypeFamilies #-}

class A e where
  type Arg e a
  f :: (Arg e a -> b) -> e a -> e b

解决方案仍然是为 FSVec n 而不是 FSVec 编写一个 A 实例。现在 n 已经移动到 instance 声明中，显然有一个地方可以捕获所需的 Nat n 上下文。

instance Nat n => A (FSVec n) where
  type Arg (FSVec n) a = FSVec n a
  f = undefined -- ...

Answer 2

Cirdec 的回答解释了其中一个问题，但它给出的解决方案并没有完全回答发布的问题。该问题要求 class A 的实例 X，具有 FSVec 类型的同义词。

此处阻止定义 type Arg X = FSVec size a（在任何可能的配置中）的首要问题是 type families are not injective。了解这一点并遵循 Cirdec 的推理，我可以想到实现此目标的解决方法：在 Xs 类型中包含一个代理 "context" 变量，以克服上述问题。

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 等多个函数时可能无法很好地扩展，因为它们之间可能会出现类型冲突推断 "contexts".

我能想到的最佳解决方案是为每个实例添加一个 constraint synonym (as suggested by this answer)，例如：

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 extension (based on injective type families) 手动证明单射性，并将 Arg 定义为：

type family Arg (e :: * -> *) context = (r :: * -> *) | r -> context

当然，如果类型族的设计不是单射的（我就是这种情况），这是不可能的，但这是迄今为止最干净的解决方案。如果可以使用 provided paper.

中的指南设计她的字体系列，绝对推荐

类型族实例中的类型级约束

Type-level constraints in instances of type families

haskell

type-constraints

type-families

上下文 + 最小工作示例

试用