別のIsoから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 

しかし、型式チェッカーはであり、確かにでこれに満足していませんでした。正確な出力は以下の通りです：

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

注

次に、我々は反転動作を実行するために型クラスを定義します論理述語をモデル化するこのアプローチの1つの制限は、すべての原子が第e式ツリー内の同じ深さ。 例えば、あなたがこの木を表すことができない（ここではx、yとzは原子である）：

   and 
      / \ 
      x or 
      /\ 
       y z 

Answer 2

liftClauseは、Iso' a aでのみ動作します。つまり、2つのドメインは同じタイプのタイプaでなければなりません。

しかしnegatingClauseは型を持つ：

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

Conjunction AtomとDisjunction Atomが同じではないので、そう、あなたがそれにliftClauseを呼び出すことはできません。

Answer 3

私はあなたがすべきかを把握するために十分な詳細でこれを読んでいないが、liftClauseは自分自身にいくつかのタイプから、すなわち同型をIso' a aかかります。 negatingClauseはIso' (Conjunction Atom) (Disjunction Atom)です。これは間違いなくIso' a aと一致しません。そのため、Conjunction AtomとDisjunction Atomを一致させることができないというタイプのエラーが発生することがあります。