使用STUArray时找不到适当的函数签名（GHC也是如此）

Question

我使用ST-Monad和非装箱STArrays (STUArray)编写了一个用于找到矩阵行列式的函数。矩阵的类型如下：

newtype Matrix e = Matrix (Array Int (UArray Int e))

即，一个不可变的数组，其中包含不可变的未装箱的数组，包含元素。这将要求我将谓词 IArray UArray e 添加到处理 Matrix 的函数中，这又需要 FlexibleContexts。好的，完成。

用于计算行列式的函数具有以下签名：

detST :: (IArray UArray e, MArray (STUArray s) e (ST s),
          Num e, Eq e, Division e)
   => Array Int (UArray Int e) -> ST s e

根据需要，我还必须添加谓词MArray (STUArray s) e (ST s)，因为内部会将数组转换为可变数组（外层包装，内部不包装）。

该函数可以像这样使用：

main = do
    let m@(Matrix x) = matrix [ [1,-2,3,234]
                              , [5,2,3,-3]
                              , [7,18,3,40]
                              , [2,9,71,0] ]
        d = runST (detST x) :: Int -- needed for type check, ambiguous otherwise

print d

运行良好。但是看看它有多丑！当然，我不想泄露Matrix的内部信息（至少不比我的函数附加的谓词更多）。我想定义以下函数：

det :: Matrix e -> e

我无法做到。

我试过没有正确的签名：

det (Matrix arr) = runST (detST arr)

失败了。好吧，我会动动脑筋： detST 需要 IArray UArray e, MArray (STUArray s) e (ST s), Num e, Eq e, Division e，那么 det 也需要，是吗？

det :: (IArray UArray e, MArray (STUArray s) e (ST s),
          Num e, Eq e, Division e) => Matrix e -> e

程序运行失败。但我不知道为什么。 GHC (7.4.2) 给我的提示信息是：

Could not deduce (MArray (STUArray s) t (ST s))
  arising from a use of `detST'

但是确切的术语在谓词中！

GHC建议：

add (MArray (STUArray s) t (ST s)) to the context of
  a type expected by the context: ST s t
  or the inferred type of
     det :: (Eq t, Num t, IArray UArray t, Division t) => Matrix t -> t
or add an instance declaration for (MArray (STUArray s) t (ST s))

好的。据我理解，我已经完成了第一件事情。而且确实存在一个实例(MArray ...)（否则，我怎么能在主函数中成功使用它呢？！）。

我不确定这里出了什么问题。我认为这与s中的“隐藏”ST状态有关，而detST中的s是与det中的s不同的另一个s，但我不知道如何为此编写类型。

det的正确定义是什么 - 为什么？！

没有det的程序通过只使用FlexibleContexts编译得很好，在-Wall下没有警告。完整的源代码可以在此处作为gist找到。

- scravy

---

首先，为什么不使用一个以(Int, Int)为索引的UArray，而不是一个数组的数组呢？ - Mikhail Glushenkov

为了方便我轻松地切换行。无论如何，当然还有其他可能的程序版本。但是我想知道为什么我不能定义那个特定的函数，以及它有什么问题。 - scravy

你能展示一下 detST 的定义，这样我们就可以测试你的代码了吗？我不太明白为什么它需要在 ST 中。 - Mikhail Glushenkov

完整的代码已链接为 gist，请参见问题的最后四个单词。由于它在内部使用 STUArray，因此需要在ST中。即 detST 是应该作为内部函数的函数，而 det 则是我将公开导出的函数。 - scravy

Answer 1

我成功地使用Keegan McAllister在这篇文章中描述的技巧使其工作：

{-# LANGUAGE FlexibleContexts, ScopedTypeVariables, RankNTypes, GADTs #-}

data Evidence s e where
  Evidence :: (MArray (STUArray s) e (ST s)) => Evidence s e

data ElemType e = ElemType (forall s. Evidence s e)

det :: forall e . (IArray UArray e, Num e, Eq e, Division e)
       => ElemType e -> Matrix e -> e
det (ElemType e) mat = runST (f e mat)
  where
    f :: Evidence s e -> Matrix e -> ST s e
    f Evidence (Matrix arr) = detST arr

使用方法：

main :: IO ()
main = do
    let m = matrix [ [1,-2,3,234]
                   , [5,2,3,-3]
                   , [7,18,3,40]
                   , [2,9,71,0] ]
    print $ det (ElemType Evidence) (m :: Matrix Int)

问题源于缺乏更高级别的约束条件 - runST 的类型为(forall s. ST s a) -> a，因此您需要一个类似于forall s . MArray (STUArray s) e (ST s)的约束条件，但这些约束条件不受GHC支持。这个技巧可以让您说服类型检查器实际上保持约束。有关此问题的更深入讨论，请参见我上面链接的文章。

- Mikhail Glushenkov