Verwendung einer Monade zur impliziten Überprüfung der Verfeinerungsart Wohlgeformtheit

Question

Bei der Implementierung eines Verfeinerungssystems muss ich sicherstellen, dass die Typen wohlgeformt sind. Zum Beispiel sollte ein Typ wie Num[100,0] nicht passieren, wobei Num[lb,ub] die Art der Zahlen größer als lb und kleiner als ub ist. Ich schrieb dann:

-- FORMATION RULES 

class RefTy t 
    where tyOK :: t -> Bool 

instance RefTy Ty 
    where tyOK (NumTy (n1, n2)) = n1 <= n2 
     tyOK (CatTy cs) = isSet cs 

{- 
data WellFormed t = Valid t 
        | Invalid 

instance Monad WellFormed 
    where 
    (>>=) :: RefTy a => WellFormed a -> (a -> WellFormed b) -> WellFormed b 
    Valid t >>= f 
      | tyOK t = f t 
      | otherwise = Invalid 
    Invalid >>= _ = Invalid 
-} 

Was mich in das bekannte Problem der "restricted Monad" bekam. Die vorgeschlagene Antwort ist die Wellformed Monade, um allgemein zu sein, aber die Funktionen einzuschränken. Das würde jedoch dazu führen, dass überall der wohlgeformte Scheck hinzugefügt wird. Gibt es einen besseren Weg, um herumzukommen?

Answer 1

In Ihrem Fall glaube ich nicht, dass Sie tatsächlich eine Monade wollen, nur der Zucker, der do Notation begleitet. Haben Sie zum Beispiel darüber nachgedacht, wie Ihre Definition von Applicative aussehen wird? Dinge werden unordentlich schnell, wenn du versuchst, deinen Weg durch diese zu betrügen.

Stattdessen, wenn Sie die do -Notation verwenden wollen, schlage ich vor, Sie verwenden

{-# LANGUAGE RebindableSyntax #-} 

, die Sie unter anderem, was die (>>=) und return verwendet in Entzuckerung einen do Block neu zu definieren, ermöglicht. Sie könnten dann schreiben so etwas wie:

myBind :: RefTy t1 => WellFormed t1 -> (t1 -> WellFormed t2) -> WellFormed t2 
myBind Invalid _ = Invalid 
myBind (Valid t) f | tyOK t = f t 
        | otherwise Invalid 

myReturn :: WellFormed t 
myReturn t = Valid t 

Ich bin nicht sicher, ich mit diesen Definitionen einverstanden sind, aber unabhängig würden Sie dann in der Lage sein, so etwas wie

do 
    ... 
    where (>>=) = myBind 
     return = myReturn