Endgültige taglose Codierung von gegenseitig rekursiven Typen

Question

Ich versuche, ein Paar gegenseitig rekursive Datentypen in der final-tagless Codierung auszudrücken.

ich in der Lage bin zu schreiben:

{-# LANGUAGE NoMonomorphismRestriction #-} 
{-# LANGUAGE ExplicitForAll #-} 
module Test where 

    class ExprSYM repr where 
    expr :: forall proc. (ProcSYM proc) => proc Int -> repr 

    class ProcSYM repr where 
    varProc :: forall a. String -> repr a 
    intProc :: String -> repr Int 
    subjectOf :: forall expr. (ExprSYM expr) => expr -> repr Int 

    myProc = intProc "proc A." 

jedoch, wenn ich schreibe:

myExpr = expr myProc 

ich die folgende Fehlermeldung:

Could not deduce (Test.ProcSYM proc0) 
    arising from a use of ‘Test.expr’ 
from the context (Test.ExprSYM repr) 
    bound by the inferred type of 
      Test.myExpr :: Test.ExprSYM repr => repr 
    at src/Test.hs:16:3-22 
The type variable ‘proc0’ is ambiguous 
In the expression: Test.expr Test.myProc 
In an equation for ‘Test.myExpr’: 
    Test.myExpr = Test.expr Test.myProc 

Hat eine solche Codierung erfordern den Einsatz von funktionalen Abhängigkeiten (oder Äquivalent), um die Beschränkung zwischen den beiden representation Typ zu testen es?

Wenn ja, wie würde ich das schreiben?

Answer 1

Start Lassen Sie uns, indem du die Art der myProc suchen

myProc :: ProcSYM repr => repr Int 
myProc = intProc "proc A." 

Dies sagt forall Arten repr wo ProcSYM repr, ich bin ein Wert vom Typ repr Int. Wenn wir mehrere Implementierungen von ProcSYM hatten, ist dies ein Wert, der in allen von ihnen polymorph ist. Zum Beispiel, wenn wir eine entsprechende markierte GADTProcSYM' mit einer ProcSYM Instanz hätten, könnte myProc als ein Wert von ProcSYM' verwendet werden.

{-# LANGUAGE GADTs #-} 

data ProcSYM' a where 
    VarProc :: String -> ProcSYM' a 
    IntProc :: String -> ProcSYM' a 

instance ProcSYM ProcSYM' where 
    varProc = VarProc 
    intProc = IntProc 

myProc' :: ProcSYM' Int 
myProc' = myProc 

Die ProcSym repr constraint in myProc :: ProcSYM repr => repr Int stellt einen Weg konstruieren repr s, was genau das ist, was myProc tut. Egal welche ProcSym repr Sie wollen, kann es eine repr Int konstruieren.

Die ProcSYM proc Einschränkung in der Art von expr :: forall proc. (ProcSYM proc) => proc Int -> repr ist irgendwie bedeutungslos. Die Bedingung ProcSYM proc stellt wieder ein Mittel zum Konstruieren von proc s bereit. Es kann uns nicht helfen, nach innen zu schauen oder dekonstruieren a proc Int. Ohne eine Möglichkeit, in proc Int s zu sehen, könnten wir auch nicht das proc Int Argument haben und stattdessen expr :: repr lesen.

Der Typ forall proc. ProcSYM proc => proc Int (der Typ von myProc) auf der anderen Seite verspricht, egal wie Sie proc s konstruieren, kann ich einen Wert dieses Typs bereitstellen. Sie wollen exprmyProc als erstes Argument übergeben, wie durch

myExpr = expr myProc 

in einer polymorphen Wert dieser Art Passing ohne eine konkrete Auswahl procRankNTypes erfordert.

class ExprSYM repr where 
    expr :: (forall proc. ProcSYM proc => proc Int) -> repr 

Die Instanz für ExprSYM können die ProcSYM Wörterbuch wählen in das erste Argument zu übergeben. Dies ermöglicht die Implementierung von expr, um die proc Int zu dekonstruieren. Wir zeigen dies anhand eines Beispiels mit GADTs, um zu sehen, was das tut. Wir werden auch die gleiche Änderung an dem Typ subjectOf vornehmen.

{-# LANGUAGE StandaloneDeriving #-} 
{-# LANGUAGE RankNTypes #-} 
{-# LANGUAGE GADTs #-} 
module Test where 

class ExprSYM repr where 
    expr :: (forall proc. ProcSYM proc => proc Int) -> repr 

class ProcSYM repr where 
    varProc :: forall a. String -> repr a 
    intProc :: String -> repr Int 
    subjectOf :: (forall expr. ExprSYM expr => expr) -> repr Int 

-- Tagged representation for ExprSYM 
data ExprSYM' where 
    Expr :: ProcSYM' Int -> ExprSYM' 
deriving instance Show ExprSYM' 

instance ExprSYM ExprSYM' where 
    expr x = Expr x -- chooses that the ProcSYM proc => proc Int must be ProcSYM' Int 

-- Tagged representation for ProcSYM 
data ProcSYM' a where 
    VarProc :: String -> ProcSYM' a 
    IntProc :: String -> ProcSYM' a 
    SubjectOf :: ExprSYM' -> ProcSYM' Int 

deriving instance Show (ProcSYM' a) 

instance ProcSYM ProcSYM' where 
    varProc = VarProc 
    intProc = IntProc 
    subjectOf x = SubjectOf x -- chooses that the ExprSYM repr => repr must be ExprSYM' 

-- myProc and myExpr with explicit type signatures 
myProc :: ProcSYM repr => repr Int 
myProc = intProc "proc A." 

myExpr :: ExprSYM repr => repr 
myExpr = expr myProc 

main = print (myExpr :: ExprSYM') 

Dies gibt einen abstrakten Syntaxbaum für myExpr aus. Wir können sehen, dass, wenn die Implementierung von expr den ProcSYM proc => proc Int Wert dekonstruieren wollte, es (und in diesem Fall) ein ProcSYM Wörterbuch liefern könnte, das Werte baut, weiß es, wie man dekonstruiert. Wir können dies im IntProc Konstruktor im gezeigten Wert sehen.