關於從另一個異構構建一個Iso的困惑

Question

我目前正在編寫一些代碼來以特定的方式來描述邏輯形式。在追求這個，我寫了下面的代碼，這使得使用的鏡頭：

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

於是，我試圖寫在下面（我認爲是）自然的方式：

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

negatingForm :: Iso' CNF DNF                        
negatingForm = liftClause negatingClause 

但是，typechecker是肯定不滿意這一點，我一點也不知道爲什麼。確切的輸出低於：

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 

我是一個有點新的鏡頭，並且真的想明白了我的誤解在這裏，以及我將如何實現所需的Iso。

Answer 1

（答案還貼到http://lpaste.net/164691）

下面是使用TypeFamilies溶液。

首先，我們將簡化設置：

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

的目標是創建的功能順序如下：

對方的

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

的F公司和G的是逆。從這些功能，我們可以 創建Iso'鏡頭：

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

我們首先創建類型的家庭Negated它作爲一種功能。 Negated a是f函數（或g函數）映射到a的類型。

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) 

例如，Negated (And (Or Atom))是類型Or (And Atom))。

接下來，我們定義了一個類型的類進行翻轉動作：

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) 

的同構的定義是現在簡單：

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 

例子：

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

注這種邏輯謂詞建模方法的侷限性在於，所有的原子都必須處於這個狀態表達式樹中的深度相同。 例如，你不能代表該樹（這裏x，y和z是原子）：

   and 
      / \ 
      x or 
      /\ 
       y z 

Answer 2

liftClause只能在Iso' a a上操作 - 即兩個域必須具有相同的類型 - 類型a。

然而negatingClause的類型是：

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

，所以你不能把它liftClause因爲Conjunction Atom和Disjunction Atom是不一樣的。

Answer 3

我還沒有足夠詳細閱讀找出你應該做的，但liftClause需要一個Iso' a a，即同構的一些類型本身。 negatingClause是Iso' (Conjunction Atom) (Disjunction Atom);這絕對不符合Iso' a a。這就是爲什麼類型錯誤是抱怨無法匹配Conjunction Atom與Disjunction Atom。