Verwirrt über den Aufbau einer Iso von einer anderen Iso

Question

Ich schreibe gerade etwas Code, um logische Formen in einer bestimmten Weise zu streiten. Bei der Verfolgung dieses habe ich den folgenden Code geschrieben, die Verwendung von Objektiven macht:

{-# LANGUAGE NoImplicitPrelude #-}    
{-# LANGUAGE Rank2Types #-} 

module Logic.Internal.Formula where 

import BasicPrelude hiding (empty, negate)   
import qualified Data.Set as Set 
import Control.Lens 

data Atom = Pos { i :: Integer}                       
      | Neg { i :: Integer}                       
      deriving (Eq, Ord, Show, Read)                     

negatingAtom :: Iso' Atom Atom                        
negatingAtom = iso go go                         
    where go (Pos x) = Neg x                         
     go (Neg x) = Pos x                         

newtype Conjunction a = Conjunction (Set a)                    
    deriving (Eq, Ord, Read, Show)                       

conjuncts :: Conjunction a -> [a]                       
conjuncts (Conjunction x) = Set.toList x                     

newtype Disjunction a = Disjunction (Set a)                    
    deriving (Eq, Ord, Read, Show) 
disjuncts :: Disjunction a -> [a]                       
disjuncts (Disjunction x) = Set.toList x                     

negatingClause :: Iso' (Conjunction Atom) (Disjunction Atom)                
negatingClause = liftClause negatingAtom                     

type CNF = Conjunction (Disjunction Atom)                     
type DNF = Disjunction (Conjunction Atom) 

-- Helper stuff                

liftClause :: (Ord a) => Iso' a a -> Iso' (Conjunction a) (Disjunction a)             
liftClause x = let pipeline = Set.fromList . fmap (view x) in                
    iso (Disjunction . pipeline . conjuncts) (Conjunction . pipeline . disjuncts) 

Dann versuchte ich folgendes in zu schreiben (was ich glaubte war), um die natürliche Art und Weise:

type CNF = Conjunction (Disjunction Atom)                     
type DNF = Disjunction (Conjunction Atom)                     

negatingForm :: Iso' CNF DNF                        
negatingForm = liftClause negatingClause 

Allerdings war der Typchecker definitiv nicht glücklich damit, und ich bin überhaupt nicht sicher, warum. Der genaue Ausgang ist unten:

Couldn't match type ‘Conjunction Atom’ with ‘Disjunction Atom’                
Expected type: p1 (Disjunction Atom) (f1 (Disjunction Atom))                
       -> p1 (Disjunction Atom) (f1 (Disjunction Atom))               
    Actual type: p1 (Disjunction Atom) (f1 (Disjunction Atom))                
       -> p1 (Conjunction Atom) (f1 (Conjunction Atom))               
In the first argument of ‘liftClause’, namely ‘negatingClause’                
In the expression: liftClause negatingClause 

ich Linsen ein bisschen neu bin, und möchte wirklich verstehen, was ich falsch verstanden hier, und wie ich die erforderlichen Iso implementieren würde.

Answer 1

(Antwort auch http://lpaste.net/164691 veröffentlicht)

Hier ist eine Lösung TypeFamilies verwenden.

Zuerst werden wir die Einrichtung vereinfachen:

{-# LANGUAGE TypeFamilies #-} 

import Control.Lens 

data Atom = Pos Int | Neg Int deriving (Show) 
newtype And a = And [a]  deriving (Show) 
newtype Or a = Or [a]  deriving (Show) 

Das Ziel ist, die folgende Abfolge von Funktionen erstellen:

f0 :: Atom -> Atom      g0 :: Atom -> Atom 
f1 :: And Atom -> Or Atom    g1 :: Or Atom -> And Atom 
f2 :: And (Or Atom) -> Or (And Atom) g1 :: Or (And Atom) -> And (Or Atom) 
... 

Die Fs und Gs sind invers zueinander sind. Aus diesen Funktionen können wir schaffen die Iso' Linsen:

iso0 = iso f0 g0 :: Iso' Atom Atom 
iso1 = iso f1 g1 :: Iso' (And Atom) (Or Atom) 
iso2 = iso f2 g2 :: Iso' (And (Or Atom)) (Or (And Atom)) 

Wir beginnen mit der Art Familie Negated zu schaffen, die als eine Art Funktion wirkt. Negated a ist der Typ, den eine f-Funktion (oder g-Funktion) a zuordnet.

type family Negated a 

type instance Negated Atom = Atom 
type instance Negated (And a) = Or (Negated a) 
type instance Negated (Or a) = And (Negated a) 

Zum Beispiel Negated (And (Or Atom)) ist der Typ Or (And Atom)).

Anschließend definieren wir eine Typ-Klasse die invertierende Operation auszuführen:

class Invertible a where 
    invert :: a -> Negated a 

instance Invertible Atom where 
    invert (Pos a) = Neg a 
    invert (Neg a) = Pos a 

instance Invertible a => Invertible (And a) where 
    invert (And clauses) = Or (map invert clauses) 

instance Invertible a => Invertible (Or a) where 
    invert (Or clauses) = And (map invert clauses) 

Die Definitionen der Isomorphien sind jetzt trivial:

iso0 :: Iso' Atom Atom 
iso0 = iso invert invert 

iso1 :: Iso' (And Atom) (Or Atom) 
iso1 = iso invert invert 

iso2 :: Iso' (And (Or Atom)) (Or (And Atom)) 
iso2 = iso invert invert 

Beispiele:

and1 = And [ Pos 1, Neg 2, Pos 3 ] 
or1 = Or [and1] 

test1 = invert and1     -- Or [Neg 1,Pos 2,Neg 3] 
test2 = invert or1     -- And [Or [Neg 1,Pos 2,Neg 3]] 

Note Eine Einschränkung dieses Ansatzes zur Modellierung logischer Prädikate ist, dass alle Atome auf th stehen müssen Die gleiche Tiefe im Ausdrucksbaum. ZB können Sie nicht diesen Baum darstellen (hier x, y und z Atome sind):

   and 
      / \ 
      x or 
      /\ 
       y z 

Answer 2

liftClause kann nur auf eine Iso' a a - d. H. Die beiden Domänen müssen den gleichen Typ haben - der Typ a.

jedoch negatingClause hat Typ:

negatingClause :: Iso' (Conjunction Atom) (Disjunction Atom) 

so kann man nicht liftClause auf nennen es seit Conjunction Atom und Disjunction Atom sind nicht das gleiche.

Answer 3

Ich habe nicht detailliert genug lesen, um herauszufinden, was Sie sollte tun, aber liftClause nimmt ein Iso' a a, das heißt einen Isomorphismus von irgendeiner Art an sich selbst. negatingClause ist ein Iso' (Conjunction Atom) (Disjunction Atom); Dies passt definitiv nicht Iso' a a. Deshalb beschwert sich der Typfehler darüber, dass Conjunction Atom nicht mit Disjunction Atom übereinstimmen kann.