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

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 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 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 []

类型推断系统似乎丢失了有关大小的信息:

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

看来您正在使用类 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 -> * -> * 。您已经遇到了问题，甚至还没有使用类型系列。如果您尝试这样做(暂时放弃类型族参数)

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