Kann keine richtige Signatur für eine Funktion mit STUArray finden (keine kann GHC)

Question

Ich baute eine Funktion zum Auffinden der Determinante einer Matrix mit der ST-Monade und unboxed STArrays (STUArray). Der Typ für eine Matrix ist die folgende:

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

, die eine unveränderliche Array mit unveränderlichen unboxed Arrays enthalten, die ist. Dazu muss ich das Prädikat IArray UArray e zu Funktionen hinzufügen, die sich auf Matrix beziehen, was wiederum FlexibleContexts erfordert. OK, erledigt.

Die Funktion verwendet die Determinante zu berechnen hat die folgende Signatur:

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

I benötigt werde, um auch die Predicate MArray (STUArray s) e (ST s) hinzuzufügen, da intern die Arrays in änderbare Arrays umgewandelt werden (die äußere eingerahmt, die innere unboxed) .

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 

Works, fein:

Diese Funktion kann wie so verwendet werden. Aber schau, wie hässlich es ist! Natürlich möchte ich nicht die Interna von Matrix verraten (zumindest nicht weiter als die Prädikate, die an meine Funktionen geknüpft sind). Ich möchte folgende Funktion definieren:

det :: Matrix e -> e 

Und ich kann nicht.

Ich habe versucht, ohne eine richtige Signatur:

det (Matrix arr) = runST (detST arr) 

ausfällt. Fair genug, ich werde mein Gehirn an die Arbeit setzen: detST erfordert IArray UArray e, MArray (STUArray s) e (ST s), Num e, Eq e, Division e, tut dies auch det, nicht wahr?

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

schlägt fehl. Aber ich sehe nicht wie. Die Nachricht, die GHC (7.4.2) gibt mir ist:

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

aber der genaue Begriff ist in den Prädikaten!

GHC schlägt vor:

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

Okay. Zu meinem Verständnis habe ich das zuerst getan. Auch gibt es eine Instanz für diese (MArray ...) (sonst, wie könnte ich es erfolgreich in main verwendet haben ?!).

Ich bin mir nicht sicher, was hier falsch ist. Ich glaube, dass es etwas mit dem "versteckten" ST-Zustand in s zu tun hat, und dass das von detST einige andere s als die s in det wäre, aber ich weiß nicht, wie man einen Typ dafür schreibt.

Was ist die richtige Definition von det - und warum ?!

Das Programm ohne det kompiliert nur mit FlexibleContexts, keine Warnungen mit -Wall.Der vollständige Quellcode kann as a gist here gefunden werden.

Answer 1

ich es geschafft, diese von Keegan McAllister in this article beschrieben mit dem Trick, um die Arbeit zu machen:

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

Verbrauch:

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) 

Das Problem aus dem Mangel an höherrangige Einschränkungen ergibt sich - runST hat Geben Sie (forall s. ST s a) -> a ein, daher benötigen Sie eine Einschränkung wie forall s . MArray (STUArray s) e (ST s), die von GHC nicht unterstützt wird. Mit diesem Trick können Sie den Typprüfer davon überzeugen, dass die Einschränkung tatsächlich gilt. Eine ausführlichere Diskussion dieses Problems ist in dem oben verlinkten Artikel verfügbar.