使用monadic rank-2类型

Question

这是代码:

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

module Foo where

import Data.Vector.Generic.Mutable as M
import Data.Vector.Generic as V
import Control.Monad.ST
import Control.Monad.Primitive
import Control.Monad

data DimFun v s r = 
  DimFun {dim::Int, func :: v (PrimState s) r -> s ()}

runFun :: (Vector v r) => 
  (forall s . (PrimMonad s) => DimFun (Mutable v) s r) -> v r -> v r
runFun t x = runST $ do
  y <- thaw x
  evalFun t y
  unsafeFreeze y

evalFun :: (PrimMonad s, MVector v r) => DimFun v s r -> v (PrimState s) r -> s ()
evalFun (DimFun dim f) y | dim == M.length y = f y

fm :: (MVector v r, PrimMonad s, Num r, Monad m) => m (DimFun v s r)
fm = error ""

f :: forall v r m . (Vector v r, Num r, Monad m) => m (v r -> v r)
f = liftM runFun $ (fm :: forall s . (PrimMonad s) => m (DimFun (Mutable v) s r))

这会导致错误:

Couldn't match type ‘DimFun (Mutable v) s0 r’
              with ‘forall (s :: * -> *). PrimMonad s => DimFun (Mutable v) s r’
Expected type: DimFun (Mutable v) s0 r -> v r -> v r
  Actual type: (forall (s :: * -> *).
                PrimMonad s =>
                DimFun (Mutable v) s r)
               -> v r -> v r
Relevant bindings include
  f :: m (v r -> v r) (bound at Testing/Foo.hs:36:1)
In the first argument of ‘liftM’, namely ‘runFun’
In the expression: liftM runFun

但是,我不确定如何修复或诊断问题.它可能就像一个好位置(和写得很好)的类型签名一样简单.

在试图弄清楚发生了什么的时候,我写了一个非monadic版本(对我来说没用),但它编译:

gm :: (MVector v r, PrimMonad s, Num r) => DimFun v s r
gm = error ""

g :: forall v r m . (Vector v r, Num r) => v r -> v r
g = runFun (gm :: forall s . (PrimMonad s) => DimFun (Mutable v) s r)

这让我觉得上面的错误与这个问题有关,那里没有字典去的地方,但那真的只是在黑暗中刺伤.

Answer 1

一种解决方案是将PrimMonad约束移至数据类型内部DimFun。

data DimFun v r = DimFun 
   { dim  :: Int
   , func :: forall s . PrimMonad s => v (PrimState s) r -> s ()
   }

代码的其余部分按原样编译，s从以下位置删除参数DimFun：

runFun :: Vector v r => DimFun (Mutable v) r -> v r -> v r
runFun = ...

evalFun :: (PrimMonad s, MVector v r) => DimFun v r -> v (PrimState s) r -> s () 
evalFun = ...

fm :: (MVector v r, Num r, Monad m) => m (DimFun v r)
fm = ...

f :: (Vector v r, Num r, Monad m) => m (v r -> v r)
f = liftM runFun fm

将类约束移动到数据类型中可能会让您感到害怕，但实际上，无论如何您已经在那里有了类约束。PrimState是 的关联类型族PrimMonad，因此为了生成或使用v (PrimState s) r，您需要PrimMonad约束。

如果您想避免这种情况，则必须更改某些内容的类型。要了解为什么您拥有的函数类型错误，请考虑以下内容（需要ImpredictiveTypes）：

fm :: (MVector v r, PrimMonad s, Num r, Monad m) => m (DimFun v s r)
fm = error ""

g :: (Vector v r, Monad m) 
  => m (forall s . PrimMonad s => DimFun (Mutable v) s r) -> m (v r -> v r)
g = liftM runFun 

应该清楚为什么g fm类型错误：g期望 位于forall s . PrimMonad s =>内部的内容m，而 的情况并非如此fm。您必须编写一个类型的函数：

fm' :: (MVector v r, Monad m, Num r) => m (forall s . PrimMonad s => DimFun v s r)
fm' = error ""

f :: forall v r m . (Vector v r, Num r, Monad m) => m (v r -> v r)
f = g fm'