Sử dụng một monadic rank-2 loại

Question

Dưới đây là các mã:

{-# 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)) 

Điều này dẫn đến lỗi:

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 

Tuy nhiên, tôi không chắc chắn làm thế nào để sửa chữa hoặc chẩn đoán vấn đề. Nó có thể đơn giản như một chữ ký loại tốt (và được viết tốt).

Trong khi cố gắng tìm ra những gì đang diễn ra, tôi viết một phiên bản không monadic (vô ích cho tôi), nhưng nó biên dịch:

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) 

Điều này làm cho tôi điều các lỗi trên có liên quan đến this question nơi không có chỗ cho từ điển để đi, nhưng đó thực sự chỉ là một đâm trong bóng tối.

Answer 1

Một giải pháp là di chuyển ràng buộc PrimMonad bên trong kiểu dữ liệu DimFun.

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

Phần còn lại của mã của bạn biên dịch như-là, loại bỏ các s tham số từ 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 

Di chuyển khó khăn lớp thành các kiểu dữ liệu có thể có vẻ đáng sợ đối với bạn, nhưng trong thực tế, bạn đã đã có sự ràng buộc của lớp ở đó. PrimState là họ nhóm có liên quan là PrimMonad, do đó, để sản xuất hoặc tiêu thụ v (PrimState s) r, bạn cần giới hạn PrimMonad.

Nếu bạn muốn tránh nó, bạn sẽ phải thay đổi loại thứ gì đó. Để xem lý do tại sao các chức năng bạn có được illtyped, hãy xem xét những điều sau đây (mà đòi hỏi 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 

Nên xóa tại sao g fm được illtyped: g hy vọng một cái gì đó nơi forall s . PrimMonad s => là bên các m, đó là không phải là trường hợp của fm. Bạn sẽ phải viết một chức năng của loại:

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'